Module

ExistsUniqueAbelianConductor.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.ExistsUniqueAbelianConductor

1 declaration indexed from sourceView source ↗

Module documentation

Unique existence of the abelian conductor

Existence of a least ray-class-field modulus and uniqueness of any modulus with the same universal property combine into a unique-existence statement.

Imports3

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

theorem

existsUnique_abelianConductor

L22 ↗

ClassFieldTheory.existsUnique_abelianConductor

Documentation

The conductor of a finite abelian extension of number fields exists uniquely.

Source context 1 command

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

namespace ClassFieldTheory

Lean source · statement

theorem existsUnique_abelianConductor
    (K : Type) [Field K] [NumberField K]
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [IsAbelianGalois K L] :
    ∃! c : RayClassModulus K, IsAbelianConductor K L c

Module documentation

Unique existence of the abelian conductor

Declarations

existsUnique_abelianConductor