CyclicCohomology.herbrand_tateCohomology_zero_units_cardinal_eq_normQuotient
Degree-zero Tate cohomology of field units is equipotent to the norm quotient.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace CyclicCohomology
open LocalFieldTheory
noncomputable sectionLean source · statement
theorem herbrand_tateCohomology_zero_units_cardinal_eq_normQuotient (K L : Type)
[Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] :
Cardinal.mk (tateCohomology (Rep.ofAlgebraAutOnUnits K L) 0) =
Cardinal.mk (Additive (NormQuotient K L))