Module

AbelianConductorRayClassFieldLe.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.AbelianConductorRayClassFieldLe

1 declaration indexed from sourceView source ↗

Module documentation

The conductor of a ray class field

The conductor of the ray class field for a modulus m is bounded above by m. Equality need not hold: a modulus may contain redundant conditions.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

theorem

le_rayClassFieldModulus

L22 ↗

ClassFieldTheory.IsAbelianConductor.le_rayClassFieldModulus

Documentation

A ray class field's conductor is at most its defining modulus.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

theorem IsAbelianConductor.le_rayClassFieldModulus
    {K : Type u} [Field K] [NumberField K]
    {m c : RayClassModulus K}
    (R : RayClassFieldRealization K m)
    (hc : IsAbelianConductor K R.extension c) :
    c ≤ m

Module documentation

The conductor of a ray class field

Declarations

le_rayClassFieldModulus