Module

ExistsAbelianConductor.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.ExistsAbelianConductor

1 declaration indexed from sourceView source ↗

Module documentation

Existence of the abelian conductor

The conductor of a finite abelian extension is the least modulus whose ray class field contains that extension. The older theorem name embedsInRayClassField_iff_conductor_le remains available for compatibility; its conclusion is an existence statement, so this name reflects its type.

Imports2

Imported by2

theorem

exists_abelianConductor

L22 ↗

ClassFieldTheory.exists_abelianConductor

Documentation

A finite abelian extension of number fields has a conductor.

Source context 1 command

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

namespace ClassFieldTheory

Lean source · statement

theorem exists_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

Existence of the abelian conductor

Declarations

exists_abelianConductor