Module

KummerAlgebraFinrank.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.KummerAlgebraFinrank

1 declaration indexed from sourceView source ↗

Module documentation

The rank of K[X] / (X ^ n - a) is n regardless of whether the polynomial is irreducible. This is distinct from the index of its norm subgroup.

Imports2

Imported by2

theorem

ClassFieldTheory.kummerAlgebra_finrank

Documentation

The Kummer algebra has the polynomial's degree as its dimension.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTheory
universe u

Lean source · statement

theorem kummerAlgebra_finrank
    (K : Type u) [Field K] (n : ℕ+) (a : Kˣ) :
    Module.finrank K (KummerAlgebra K n a) = (n : ℕ)