theorem CosetDensity.dirichletDensity_coprime_primes_eq_one (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (_h_cong : GlobalCFT.IsCongruenceSubgroup K 𝔪 𝒞) : RayClassField.DirichletDensity K {𝔭 : RayClassField.Prime' K | ∃ (_ : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0), True} = some 1

theorem CosetDensity.dirichletDensity_coset_partition_sum (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) (reps : Fin n → RayClassField.FracIdealsCoprime K 𝔪) (h_reps : Function.Injective fun (i : Fin n) => ↑(reps i)) : (RayClassField.DirichletDensity K {𝔭 : RayClassField.Prime' K | ∃ (_ : 𝔪.toFun (RayClassField.Place.finite 𝔭) = 0), True}).getD 0 = ∑ i : Fin n, GlobalCFT.dirichletDensityCoset K 𝔪 𝒞 h_cong (reps i)

theorem CosetDensity.density_cosets_sum_one (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) (reps : Fin n → RayClassField.FracIdealsCoprime K 𝔪) (h_reps : Function.Injective fun (i : Fin n) => ↑(reps i)) : ∑ i : Fin n, GlobalCFT.dirichletDensityCoset K 𝔪 𝒞 h_cong (reps i) = 1

theorem CosetDensity.corollary_22_22 (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) (reps : Fin n → RayClassField.FracIdealsCoprime K 𝔪) (h_reps : Function.Injective fun (i : Fin n) => ↑(reps i)) : GlobalCFT.AllLValuesNonzero K 𝔪 𝒞 ∧ ∀ (I : RayClassField.FracIdealsCoprime K 𝔪), GlobalCFT.dirichletDensityCoset K 𝔪 𝒞 h_cong I = 1 / ↑n