theorem RayClassField.Modulus.gcd_dvd_left {K : Type u} [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) : (𝔪₁.gcd 𝔪₂).dvd 𝔪₁

theorem RayClassField.Modulus.gcd_dvd_right {K : Type u} [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) : (𝔪₁.gcd 𝔪₂).dvd 𝔪₂

theorem RayClassField.Modulus.dvd_lcm_left {K : Type u} [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) : 𝔪₁.dvd (𝔪₁.lcm 𝔪₂)

theorem RayClassField.Modulus.dvd_lcm_right {K : Type u} [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) : 𝔪₂.dvd (𝔪₁.lcm 𝔪₂)

theorem RayClassField.weak_approx_ray_gen_aux' {K : Type u} [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) (α : Kˣ) (hα_cop : ∀ (v : FinitePlace K), (𝔪₁.gcd 𝔪₂).toFun (Place.finite v) ≠ 0 → (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑α = 1) (hα_val : ∀ (v : FinitePlace K), (𝔪₁.gcd 𝔪₂).toFun (Place.finite v) ≠ 0 → (IsDedekindDomain.HeightOneSpectrum.valuation K v) (↑α - 1) ≤ ↑(Multiplicative.ofAdd (-↑((𝔪₁.gcd 𝔪₂).toFun (Place.finite v))))) (hα_sign : ∀ (w : NumberField.InfinitePlace K), (𝔪₁.gcd 𝔪₂).toFun (Place.infinite w) ≠ 0 → 0 < (w.embedding ↑α).re) : ∃ (β : Kˣ), (∀ (v : FinitePlace K), 𝔪₁.toFun (Place.finite v) ≠ 0 → (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑(α * β) = 1) ∧ (∀ (v : FinitePlace K), 𝔪₁.toFun (Place.finite v) ≠ 0 → (IsDedekindDomain.HeightOneSpectrum.valuation K v) (↑(α * β) - 1) ≤ ↑(Multiplicative.ofAdd (-↑(𝔪₁.toFun (Place.finite v))))) ∧ (∀ (w : NumberField.InfinitePlace K), 𝔪₁.toFun (Place.infinite w) ≠ 0 → 0 < (w.embedding ↑(α * β)).re) ∧ (∀ (v : FinitePlace K), 𝔪₂.toFun (Place.finite v) ≠ 0 → (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑β⁻¹ = 1) ∧ (∀ (v : FinitePlace K), 𝔪₂.toFun (Place.finite v) ≠ 0 → (IsDedekindDomain.HeightOneSpectrum.valuation K v) (↑β⁻¹ - 1) ≤ ↑(Multiplicative.ofAdd (-↑(𝔪₂.toFun (Place.finite v))))) ∧ ∀ (w : NumberField.InfinitePlace K), 𝔪₂.toFun (Place.infinite w) ≠ 0 → 0 < (w.embedding ↑β⁻¹).re

theorem RayClassField.weak_approx_coprime_CRT_aux {K : Type u} [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) (J : (FracIdeal K)ˣ) (hJ : J ∈ FracIdealsCoprime_subgroup K 𝔪₁) : ∃ (a : (FracIdeal K)ˣ) (b : (FracIdeal K)ˣ), a ∈ FracIdealsCoprime_subgroup K 𝔪₂ ∧ b ∈ FracIdealsCoprime_subgroup K 𝔪₁ ∧ b ∈ RayGroup.toAmbientSubgroup K (𝔪₁.gcd 𝔪₂) ∧ J = a * b

theorem RayClassField.theorem_8_5_ray_gen_decomp {K : Type u} [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) (I : FracIdealsCoprime K (𝔪₁.gcd 𝔪₂)) (hI : IsRayGenerator (𝔪₁.gcd 𝔪₂) I) : ∃ (I₁ : FracIdealsCoprime K 𝔪₁) (I₂ : FracIdealsCoprime K 𝔪₂), IsRayGenerator 𝔪₁ I₁ ∧ IsRayGenerator 𝔪₂ I₂ ∧ (FracIdealsCoprime_subgroup K (𝔪₁.gcd 𝔪₂)).subtype I = (FracIdealsCoprime_subgroup K 𝔪₁).subtype I₁ * (FracIdealsCoprime_subgroup K 𝔪₂).subtype I₂

theorem RayClassField.ray_generator_gcd_decomp_aux {K : Type u} [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) (I : FracIdealsCoprime K (𝔪₁.gcd 𝔪₂)) (hI : IsRayGenerator (𝔪₁.gcd 𝔪₂) I) : ∃ (I₁ : FracIdealsCoprime K 𝔪₁) (I₂ : FracIdealsCoprime K 𝔪₂), IsRayGenerator 𝔪₁ I₁ ∧ IsRayGenerator 𝔪₂ I₂ ∧ (FracIdealsCoprime_subgroup K (𝔪₁.gcd 𝔪₂)).subtype I = (FracIdealsCoprime_subgroup K 𝔪₁).subtype I₁ * (FracIdealsCoprime_subgroup K 𝔪₂).subtype I₂

theorem RayClassField.ray_generator_gcd_decomp {K : Type u} [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) (I : FracIdealsCoprime K (𝔪₁.gcd 𝔪₂)) (hI : IsRayGenerator (𝔪₁.gcd 𝔪₂) I) : ∃ (J₁ : (FracIdeal K)ˣ) (J₂ : (FracIdeal K)ˣ), J₁ ∈ RayGroup.toAmbientSubgroup K 𝔪₁ ∧ J₂ ∈ RayGroup.toAmbientSubgroup K 𝔪₂ ∧ (FracIdealsCoprime_subgroup K (𝔪₁.gcd 𝔪₂)).subtype I = J₁ * J₂

theorem RayClassField.ray_generator_gcd_mem_sup {K : Type u} [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) (I : FracIdealsCoprime K (𝔪₁.gcd 𝔪₂)) (hI : IsRayGenerator (𝔪₁.gcd 𝔪₂) I) : (FracIdealsCoprime_subgroup K (𝔪₁.gcd 𝔪₂)).subtype I ∈ RayGroup.toAmbientSubgroup K 𝔪₁ ⊔ RayGroup.toAmbientSubgroup K 𝔪₂

theorem RayClassField.theorem_8_5_ray_group_gcd (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) : RayGroup.toAmbientSubgroup K (𝔪₁.gcd 𝔪₂) ≤ RayGroup.toAmbientSubgroup K 𝔪₁ ⊔ RayGroup.toAmbientSubgroup K 𝔪₂

theorem RayClassField.theorem_8_5_coprime_CRT_bridge (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) : FracIdealsCoprime_subgroup K 𝔪₁ ≤ FracIdealsCoprime_subgroup K 𝔪₂ ⊔ FracIdealsCoprime_subgroup K 𝔪₁ ⊓ RayGroup.toAmbientSubgroup K (𝔪₁.gcd 𝔪₂)

theorem RayClassField.theorem_8_5_coprime_CRT_core (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) : FracIdealsCoprime_subgroup K 𝔪₁ ≤ FracIdealsCoprime_subgroup K 𝔪₂ ⊔ FracIdealsCoprime_subgroup K 𝔪₁ ⊓ RayGroup.toAmbientSubgroup K (𝔪₁.gcd 𝔪₂)

theorem RayClassField.theorem_8_5_coprime_decomp (K : Type u) [Field K] [NumberField K] (𝔪₁ 𝔪₂ : Modulus K) : FracIdealsCoprime_subgroup K 𝔪₁ ≤ FracIdealsCoprime_subgroup K 𝔪₁ ⊓ FracIdealsCoprime_subgroup K 𝔪₂ ⊔ FracIdealsCoprime_subgroup K 𝔪₁ ⊓ RayGroup.toAmbientSubgroup K (𝔪₁.gcd 𝔪₂)

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

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

theorem RayClassField.equiv_sup_ray_gcd_eq {K : Type u} [Field K] [NumberField K] (p₁ p₂ : CongruenceSubgroupPair K) (hequiv : p₁.IsEquiv p₂) : p₁.toAmbientSubgroup ⊔ RayGroup.toAmbientSubgroup K (p₁.modulus.gcd p₂.modulus) = p₂.toAmbientSubgroup ⊔ RayGroup.toAmbientSubgroup K (p₁.modulus.gcd p₂.modulus)

theorem RayClassField.proposition_22_6 {K : Type u} [Field K] [NumberField K] (p₁ p₂ : CongruenceSubgroupPair K) (hequiv : p₁.IsEquiv p₂) : ∃ (p : CongruenceSubgroupPair K), p.modulus = p₁.modulus.gcd p₂.modulus ∧ p₁.IsEquiv p ∧ p₂.IsEquiv p