NYLL
Module

KummerAlgebraNormSubgroup.lean

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.KummerAlgebraNormSubgroup
1 declaration indexed from sourceView source ↗

Module documentation

Norm subgroup of a Kummer algebra

This is the image of the determinant norm on units of K[X] / (X^n - a). The algebra need not be a field, so this subgroup is defined without any irreducibility assumption on the polynomial.

Imports2
Imported by5

Declarations

def

kummerAlgebraNormSubgroup

L25 ↗
ClassFieldTheory.kummerAlgebraNormSubgroup
Documentation

The unit-norm image of the possibly reducible Kummer algebra.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u
Lean source · statement
def kummerAlgebraNormSubgroup
    (K : Type u) [Field K] (n : ℕ+) (a : Kˣ) : Subgroup Kˣ

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