theorem RayClassField.Modulus.ext_iff {K : Type u} [Field K] [NumberField K] (𝔪 𝔫 : Modulus K) : 𝔪 = 𝔫 ↔ ∀ (v : Place K), 𝔪.toFun v = 𝔫.toFun v

theorem RayClassField.Modulus.dvd_antisymm {K : Type u} [Field K] [NumberField K] (𝔪 𝔫 : Modulus K) (h₁ : 𝔪.dvd 𝔫) (h₂ : 𝔫.dvd 𝔪) : 𝔪 = 𝔫

theorem RayClassField.proposition_22_9 {K : Type u} [Field K] [NumberField K] (p p₀ : CongruenceSubgroupPair K) (hmod : p₀.modulus = p.modulus) (hprim : p.IsPrimitive) (hle : p₀.toAmbientSubgroup ≤ p.toAmbientSubgroup) : p₀.conductor = p.modulus