NYLL
Module

KummerAlgebraFiniteFree.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.KummerAlgebraFiniteFree
1 declaration indexed from sourceView source ↗

Module documentation

Finite freeness of a Kummer algebra

The polynomial X ^ n - a is monic for positive n. Its quotient algebra is finite free even when that polynomial is reducible, so no field assumption is placed on the Kummer algebra.

Imports2
Imported by2

Declarations

theorem

kummerAlgebra_finiteFree

L24 ↗
ClassFieldTheory.kummerAlgebra_finiteFree
Documentation

A Kummer algebra is finite free over its base field, including reducible and degree-one cases.

Source context 2 commands

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

namespace ClassFieldTheory
universe u
Lean source · statement
theorem kummerAlgebra_finiteFree
    (K : Type u) [Field K] (n : ℕ+) (a : Kˣ) :
    Module.Finite K (KummerAlgebra K n a) ∧
      Module.Free K (KummerAlgebra K n a)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.