ClassFieldTheory.kummerAlgebraNormSubgroup_index_eq_radicalDegree
The unit-norm image of a possibly reducible Kummer algebra has index equal to the degree of a simple radical field, not necessarily n.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheoryLean source · statement
theorem kummerAlgebraNormSubgroup_index_eq_radicalDegree
(K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
(hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ) :
∃ β : SeparableClosure K,
β ^ (n : ℕ) = algebraMap K (SeparableClosure K) (a : K) ∧
(kummerAlgebraNormSubgroup K n a).index =
Module.finrank K (IntermediateField.adjoin K {β})