theorem RayClassField.Modulus.dvd_trans' {K : Type u} [Field K] [NumberField K] {𝔪₁ 𝔪₂ 𝔪₃ : Modulus K} (h₁₂ : 𝔪₁.dvd 𝔪₂) (h₂₃ : 𝔪₂.dvd 𝔪₃) : 𝔪₁.dvd 𝔪₃

theorem RayClassField.Modulus.dvd_refl {K : Type u} [Field K] [NumberField K] (𝔪 : Modulus K) : 𝔪.dvd 𝔪

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

theorem RayClassField.CongruenceSubgroupPair.isEquiv_refl {K : Type u} [Field K] [NumberField K] (p : CongruenceSubgroupPair K) : p.IsEquiv p

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

theorem RayClassField.CongruenceSubgroupPair.IsEquiv.trans_of_dvd {K : Type u} [Field K] [NumberField K] {p₁ p₂ p₃ : CongruenceSubgroupPair K} (h₁₂ : p₁.IsEquiv p₂) (h₂₃ : p₂.IsEquiv p₃) (hdvd₁ : p₂.modulus.dvd p₁.modulus) (hdvd₃ : p₂.modulus.dvd p₃.modulus) : p₁.IsEquiv p₃

theorem RayClassField.isEquiv_chain {K : Type u} [Field K] [NumberField K] {p₁ p₂ p₃ : CongruenceSubgroupPair K} (h₁₂ : p₁.IsEquiv p₂) (h₂₃ : p₂.IsEquiv p₃) (hdvd₁₂ : p₂.modulus.dvd p₁.modulus) (hdvd₂₃ : p₃.modulus.dvd p₂.modulus) : p₁.IsEquiv p₃

theorem RayClassField.IsRayGenerator_of_dvd {K : Type u} [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) (h : 𝔪₁.dvd 𝔪₂) (I : FracIdealsCoprime K 𝔪₂) (hI : IsRayGenerator 𝔪₂ I) : IsRayGenerator 𝔪₁ ((Subgroup.inclusion ⋯) I)

theorem RayClassField.RayGroup_inclusion_le {K : Type u} [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) (h : 𝔪₁.dvd 𝔪₂) (x : FracIdealsCoprime K 𝔪₂) : x ∈ RayGroup K 𝔪₂ → (Subgroup.inclusion ⋯) x ∈ RayGroup K 𝔪₁

theorem RayClassField.RayGroup_toAmbientSubgroup_antitone (K : Type u) [Field K] [NumberField K] {𝔪₁ 𝔪₂ : Modulus K} (h : 𝔪₁.dvd 𝔪₂) : RayGroup.toAmbientSubgroup K 𝔪₂ ≤ RayGroup.toAmbientSubgroup K 𝔪₁

theorem RayClassField.trans_of_dvd_reverse {K : Type u} [Field K] [NumberField K] {p₁ p₂ p₃ : CongruenceSubgroupPair K} (h₁₂ : p₁.IsEquiv p₂) (h₂₃ : p₂.IsEquiv p₃) (hdvd₁ : p₁.modulus.dvd p₂.modulus) (hdvd₃ : p₃.modulus.dvd p₂.modulus) : p₁.IsEquiv p₃

theorem RayClassField.CongruenceSubgroupPair.IsEquiv.trans' {K : Type u} [Field K] [NumberField K] {p₁ p₂ p₃ : CongruenceSubgroupPair K} (h₁₂ : p₁.IsEquiv p₂) (h₂₃ : p₂.IsEquiv p₃) : p₁.IsEquiv p₃

noncomputable def RayClassField.Modulus.weight {K : Type u} [Field K] [NumberField K] (𝔪 : Modulus K) : ℕ

theorem RayClassField.Modulus.gcd_weight_lt_of_not_dvd {K : Type u} [Field K] [NumberField K] {𝔪₁ 𝔪₂ : Modulus K} (h : ¬𝔪₁.dvd 𝔪₂) : (𝔪₁.gcd 𝔪₂).weight < 𝔪₁.weight

theorem RayClassField.corollary_22_7_existence {K : Type u} [Field K] [NumberField K] (p : CongruenceSubgroupPair K) : ∃ (p₀ : CongruenceSubgroupPair K), p.IsEquiv p₀ ∧ ∀ (q : CongruenceSubgroupPair K), p.IsEquiv q → p₀.modulus.dvd q.modulus

theorem RayClassField.corollary_22_7_modulus_unique {K : Type u} [Field K] [NumberField K] (p p₀ p₀' : CongruenceSubgroupPair K) (hp₀ : p.IsEquiv p₀) (hp₀_min : ∀ (q : CongruenceSubgroupPair K), p.IsEquiv q → p₀.modulus.dvd q.modulus) (hp₀' : p.IsEquiv p₀') (hp₀'_min : ∀ (q : CongruenceSubgroupPair K), p.IsEquiv q → p₀'.modulus.dvd q.modulus) : p₀.modulus = p₀'.modulus

theorem RayClassField.corollary_22_7 {K : Type u} [Field K] [NumberField K] (p : CongruenceSubgroupPair K) : ∃! 𝔠 : Modulus K, (∃ (p₀ : CongruenceSubgroupPair K), p₀.modulus = 𝔠 ∧ p.IsEquiv p₀) ∧ ∀ (q : CongruenceSubgroupPair K), p.IsEquiv q → 𝔠.dvd q.modulus