noncomputable def RayClassField.RayGroup.toAmbientSubgroup (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup (FracIdeal K)ˣ

theorem RayClassField.RayGroup.toAmbientSubgroup_le {K : Type u} [Field K] [NumberField K] (𝔪 : Modulus K) : toAmbientSubgroup K 𝔪 ≤ FracIdealsCoprime_subgroup K 𝔪

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

theorem RayClassField.CongruenceSubgroupPair.toAmbientSubgroup_le {K : Type u} [Field K] [NumberField K] (p : CongruenceSubgroupPair K) : p.toAmbientSubgroup ≤ FracIdealsCoprime_subgroup K p.modulus

theorem RayClassField.lemma_22_5_necessity {K : Type u} [Field K] [NumberField K] (p₁ p₂ : CongruenceSubgroupPair K) (_hdvd : p₂.modulus.dvd p₁.modulus) (hequiv : p₁.IsEquiv p₂) : FracIdealsCoprime_subgroup K p₁.modulus ⊓ RayGroup.toAmbientSubgroup K p₂.modulus ≤ p₁.toAmbientSubgroup

theorem RayClassField.lemma_22_5_sufficiency {K : Type u} [Field K] [NumberField K] (p₁ : CongruenceSubgroupPair K) (𝔪₂ : Modulus K) (hdvd : 𝔪₂.dvd p₁.modulus) (hcond : FracIdealsCoprime_subgroup K p₁.modulus ⊓ RayGroup.toAmbientSubgroup K 𝔪₂ ≤ p₁.toAmbientSubgroup) : ∃ (p₂ : CongruenceSubgroupPair K), p₂.modulus = 𝔪₂ ∧ p₁.IsEquiv p₂ ∧ p₂.toAmbientSubgroup = p₁.toAmbientSubgroup ⊔ RayGroup.toAmbientSubgroup K 𝔪₂

theorem RayClassField.lemma_22_5 {K : Type u} [Field K] [NumberField K] (p₁ : CongruenceSubgroupPair K) (𝔪₂ : Modulus K) (hdvd : 𝔪₂.dvd p₁.modulus) : (∃ (p₂ : CongruenceSubgroupPair K), p₂.modulus = 𝔪₂ ∧ p₁.IsEquiv p₂) ↔ FracIdealsCoprime_subgroup K p₁.modulus ⊓ RayGroup.toAmbientSubgroup K 𝔪₂ ≤ p₁.toAmbientSubgroup