Documentation

Atlas.NumberTheoryI.code.Def2213

source
def RayClassField.RayClassChar.kernelSubgroup {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) :
Subgroup (FracIdealsCoprime K 𝔪)
Instances For
    source
    theorem RayClassField.RayClassChar.rayGroup_le_kernelSubgroup {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) :
    RayGroup K 𝔪 ≤ χ.kernelSubgroup
    source
    def RayClassField.RayClassChar.kernelCongruenceSubgroup {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) :
    CongruenceSubgroupPair K
    Instances For
      source
      noncomputable def RayClassField.RayClassChar.conductor {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) :
      Modulus K
      Instances For
        source
        theorem RayClassField.RayClassChar.conductor_dvd {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) :
        χ.conductor.dvd 𝔪