noncomputable def RayClassField.conductorModulus {K : Type u} [Field K] [NumberField K] (p : CongruenceSubgroupPair K) : Modulus K

theorem RayClassField.conductorModulus_witness_spec {K : Type u} [Field K] [NumberField K] (p : CongruenceSubgroupPair K) : p.IsEquiv ⋯.choose ∧ ∀ (q : CongruenceSubgroupPair K), p.IsEquiv q → (conductorModulus p).dvd q.modulus

theorem RayClassField.conductorModulus_dvd {K : Type u} [Field K] [NumberField K] (p : CongruenceSubgroupPair K) : (conductorModulus p).dvd p.modulus

theorem RayClassField.conductorModulus_dvd_of_equiv {K : Type u} [Field K] [NumberField K] (p p' : CongruenceSubgroupPair K) (h : p.IsEquiv p') : (conductorModulus p).dvd p'.modulus

theorem RayClassField.conductorModulus_eq_of_equiv {K : Type u} [Field K] [NumberField K] (p₁ p₂ : CongruenceSubgroupPair K) (h : p₁.IsEquiv p₂) : conductorModulus p₁ = conductorModulus p₂

theorem RayClassField.conductorModulus_exists_equiv {K : Type u} [Field K] [NumberField K] (p : CongruenceSubgroupPair K) : ∃ (p' : CongruenceSubgroupPair K), p'.modulus = conductorModulus p ∧ p.IsEquiv p'

noncomputable def RayClassField.CongruenceSubgroupPair.conductor {K : Type u} [Field K] [NumberField K] (p : CongruenceSubgroupPair K) : Modulus K

def RayClassField.CongruenceSubgroupPair.IsPrimitive {K : Type u} [Field K] [NumberField K] (p : CongruenceSubgroupPair K) : Prop

theorem RayClassField.CongruenceSubgroupPair.conductor_dvd {K : Type u} [Field K] [NumberField K] (p : CongruenceSubgroupPair K) : p.conductor.dvd p.modulus

theorem RayClassField.CongruenceSubgroupPair.conductor_dvd_of_equiv {K : Type u} [Field K] [NumberField K] (p p' : CongruenceSubgroupPair K) (h : p.IsEquiv p') : p.conductor.dvd p'.modulus

theorem RayClassField.CongruenceSubgroupPair.conductor_eq_of_equiv {K : Type u} [Field K] [NumberField K] (p₁ p₂ : CongruenceSubgroupPair K) (h : p₁.IsEquiv p₂) : p₁.conductor = p₂.conductor