theorem CosetDensity.coset_density_eq_formula (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : GlobalCFT.IsCongruenceSubgroup K 𝔪 𝒞) (n : ℕ) (hn : 𝒞.index = n) (hn_pos : 0 < n) (I : RayClassField.FracIdealsCoprime K 𝔪) : GlobalCFT.dirichletDensityCoset K 𝔪 𝒞 h_cong I = (1 - ↑(DirichletDensity.sumOrdersNonprincipal K 𝔪 𝒞 h_cong)) / ↑n

theorem CosetDensity.coset_density_nonneg (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : GlobalCFT.IsCongruenceSubgroup K 𝔪 𝒞) (I : RayClassField.FracIdealsCoprime K 𝔪) : 0 ≤ GlobalCFT.dirichletDensityCoset K 𝔪 𝒞 h_cong I

theorem CosetDensity.proposition_22_21 (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : GlobalCFT.IsCongruenceSubgroup K 𝔪 𝒞) (n : ℕ) (hn : 𝒞.index = n) (hn_pos : 0 < n) (I : RayClassField.FracIdealsCoprime K 𝔪) : (GlobalCFT.AllLValuesNonzero K 𝔪 𝒞 → GlobalCFT.dirichletDensityCoset K 𝔪 𝒞 h_cong I = 1 / ↑n) ∧ (¬GlobalCFT.AllLValuesNonzero K 𝔪 𝒞 → GlobalCFT.dirichletDensityCoset K 𝔪 𝒞 h_cong I = 0)

theorem Prop2221.proposition_22_21 (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : GlobalCFT.IsCongruenceSubgroup K 𝔪 𝒞) (n : ℕ) (hn : 𝒞.index = n) (hn_pos : 0 < n) (I : RayClassField.FracIdealsCoprime K 𝔪) : (GlobalCFT.AllLValuesNonzero K 𝔪 𝒞 → GlobalCFT.dirichletDensityCoset K 𝔪 𝒞 h_cong I = 1 / ↑n) ∧ (¬GlobalCFT.AllLValuesNonzero K 𝔪 𝒞 → GlobalCFT.dirichletDensityCoset K 𝔪 𝒞 h_cong I = 0)