ClassFieldTheory.kummerAlgebraNormSubgroup_index_eq_powerClassOrder
Over a nonarchimedean local field containing μₙ, the norm index of K[X]/(Xⁿ-a) is the order of the class of a modulo n-th powers.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe uLean source · statement
theorem kummerAlgebraNormSubgroup_index_eq_powerClassOrder
(K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
(hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ) :
(kummerAlgebraNormSubgroup K n a).index =
orderOf (powerClass K n a)