Module

KummerExponentTower.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.KummerExponentTower

1 declaration indexed from sourceView source ↗

Module documentation

Divisibility of simple Kummer extensions

If m ∣ n and the base contains μₘ, an m-th root of a differs from the (n/m)-th power of an n-th root by a base-field root of unity. Thus the chosen simple extensions form an actual tower in the separable closure.

Imports2

Imported by2

theorem

chosenSimpleKummerExtension_le_of_dvd

L24 ↗

LocalClassFieldTheory.Kummer.chosenSimpleKummerExtension_le_of_dvd

Documentation

A simple m-Kummer extension is contained in the corresponding n-Kummer extension when m ∣ n.

Source context 2 commands

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

noncomputable section
namespace LocalClassFieldTheory.Kummer

Lean source · statement

theorem chosenSimpleKummerExtension_le_of_dvd
    (K : Type) [Field K]
    (m n : ℕ+) (hmK : ((m : ℕ) : K) ≠ 0)
    (hnK : ((n : ℕ) : K) ≠ 0)
    (hmuM : (primitiveRoots (m : ℕ) K).Nonempty)
    (hmn : (m : ℕ) ∣ (n : ℕ)) (a : Kˣ) :
    KummerTheory.chosenSimpleKummerExtension K m hmK a ≤
      KummerTheory.chosenSimpleKummerExtension K n hnK a

Module documentation

Divisibility of simple Kummer extensions

Declarations

chosenSimpleKummerExtension_le_of_dvd