theorem DirichletDensity.allLValuesNonzero_iff_orders_zero (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) : GlobalCFT.AllLValuesNonzero K 𝔪 𝒞 ↔ ∀ (χ : GlobalCFT.PrimitiveCharsContaining K 𝔪 𝒞), ¬GlobalCFT.isPrincipalPrimitive K 𝔪 𝒞 χ → GlobalCFT.orderOfVanishingPrimitive K 𝔪 𝒞 χ = 0

noncomputable def DirichletDensity.sumOrdersNonprincipal (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (_h_cong : GlobalCFT.IsCongruenceSubgroup K 𝔪 𝒞) : ℕ

theorem DirichletDensity.allLValuesNonzero_iff_sumOrders_eq_zero (K : Type u) [Field K] [NumberField K] (𝔪 : RayClassField.Modulus K) (𝒞 : Subgroup (RayClassField.FracIdealsCoprime K 𝔪)) (h_cong : GlobalCFT.IsCongruenceSubgroup K 𝔪 𝒞) : GlobalCFT.AllLValuesNonzero K 𝔪 𝒞 ↔ sumOrdersNonprincipal K 𝔪 𝒞 h_cong = 0

theorem DirichletDensity.dirichlet_density_congruence_subgroup (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) : (GlobalCFT.AllLValuesNonzero K 𝔪 𝒞 → GlobalCFT.dirichletDensityCongruence K 𝔪 𝒞 h_cong = 1 / ↑n) ∧ (¬GlobalCFT.AllLValuesNonzero K 𝔪 𝒞 → GlobalCFT.dirichletDensityCongruence K 𝔪 𝒞 h_cong = 0)