Module

KummerAlgebra.lean

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.KummerAlgebra

1 declaration indexed from sourceView source ↗

Module documentation

Imports1

Imported by12

abbrev

ClassFieldTheory.KummerAlgebra

Documentation

The Kummer algebra K[X] / (X^n - a). It remains canonical when the polynomial is reducible, so no root in a chosen closure is required.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

abbrev KummerAlgebra
    (K : Type u) [Field K] (n : ℕ+) (a : Kˣ)