Documentation

Atlas.NumberTheoryI.code.GlobalCFTMain

source
structure GlobalCFT.CongruenceSubgroup (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) :
Type u
Instances For
    source
    def GlobalCFT.CongruenceSubgroup.mk' {K : Type u} [Field K] [NumberField K] {𝔪 : RayClassField.Modulus K} (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h : IsCongruenceSubgroup K 𝔪 𝒞) :
    CongruenceSubgroup K 𝔪
    Instances For
      source
      @[implicit_reducible]
      instance GlobalCFT.instCoeOutCongruenceSubgroupSubgroupFracIdealsCoprime {K : Type u} [Field K] [NumberField K] {𝔪 : RayClassField.Modulus K} :
      CoeOut (CongruenceSubgroup K 𝔪) (Subgroup (RayClassField.FracIdealsCoprime K 𝔪))
      source
      theorem GlobalCFT.CongruenceSubgroup.ext {K : Type u} [Field K] [NumberField K] {𝔪 : RayClassField.Modulus K} {𝒞₁ 𝒞₂ : CongruenceSubgroup K 𝔪} (h : 𝒞₁.toSubgroup = 𝒞₂.toSubgroup) :
      𝒞₁ = 𝒞₂
      source
      theorem GlobalCFT.CongruenceSubgroup.ext_iff {K : Type u} [Field K] [NumberField K] {𝔪 : RayClassField.Modulus K} {𝒞₁ 𝒞₂ : CongruenceSubgroup K 𝔪} :
      𝒞₁ = 𝒞₂ ↔ 𝒞₁.toSubgroup = 𝒞₂.toSubgroup
      source
      def GlobalCFT.CongruenceSubgroup.ray {K : Type u} [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) :
      CongruenceSubgroup K 𝔪
      Instances For
        source
        def GlobalCFT.CongruenceSubgroup.top {K : Type u} [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) :
        CongruenceSubgroup K 𝔪
        Instances For
          source
          noncomputable def GlobalCFT.CongruenceSubgroup.index {K : Type u} [Field K] [NumberField K] {𝔪 : RayClassField.Modulus K} (𝒞 : CongruenceSubgroup K 𝔪) :
          ℕ
          Instances For