@[reducible, inline]

abbrev CharacterGroup (G : Type u_1) [CommGroup G] [Fintype G] : Type u_1

@[implicit_reducible]

instance CharacterGroup.instCommGroup {G : Type u_1} [CommGroup G] [Fintype G] : CommGroup (CharacterGroup G)

instance CharacterGroup.hasEnoughRootsOfUnity_complex_exponent {G : Type u_1} [CommGroup G] [Fintype G] : HasEnoughRootsOfUnity ℂ (Monoid.exponent G)

instance CharacterGroup.instFinite {G : Type u_1} [CommGroup G] [Fintype G] : Finite (CharacterGroup G)

theorem CharacterGroup.prop_18_33_mulEquiv {G : Type u_1} [CommGroup G] [Fintype G] : Nonempty (CharacterGroup G ≃* G)

theorem CharacterGroup.cor_18_34 {G : Type u_1} [CommGroup G] [Fintype G] (g : G) : g = 1 ↔ ∀ (χ : CharacterGroup G), χ g = 1

theorem CharacterGroup.cor_18_34_part2 {G : Type u_1} [CommGroup G] [Fintype G] (χ : CharacterGroup G) : χ = 1 ↔ ∀ (g : G), χ g = 1

theorem CharacterGroup.characters_separate_points {G : Type u_1} [CommGroup G] [Fintype G] : (∀ (g : G), g = 1 ↔ ∀ (χ : CharacterGroup G), χ g = 1) ∧ ∀ (χ : CharacterGroup G), χ = 1 ↔ ∀ (g : G), χ g = 1

noncomputable def conductorOfDirichletChar {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : ℕ

theorem DirichletCharacter.thm_18_13_existence {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : χ.primitiveCharacter.IsPrimitive ∧ (changeLevel ⋯) χ.primitiveCharacter = χ

theorem DirichletCharacter.thm_18_13_unique_level {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (hn : n ≠ 0) {m : ℕ} (hm : m ∣ n) (χ' : DirichletCharacter R m) (hind : (changeLevel hm) χ' = χ) (hprim : χ'.IsPrimitive) : m = χ.conductor

theorem DirichletCharacter.thm_18_13_unique_char {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (hn : n ≠ 0) (hm : χ.conductor ∣ n) (χ' : DirichletCharacter R χ.conductor) (hind : (changeLevel hm) χ' = χ) (hprim : χ'.IsPrimitive) : χ' = χ.primitiveCharacter

theorem DirichletCharacter.thm_18_13 {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (hn : n ≠ 0) : (χ.primitiveCharacter.IsPrimitive ∧ (changeLevel ⋯) χ.primitiveCharacter = χ) ∧ ∀ {m : ℕ} (hm : m ∣ n) (χ' : DirichletCharacter R m), (changeLevel hm) χ' = χ → χ'.IsPrimitive → ∃ (heq : m = χ.conductor), heq ▸ χ' = χ.primitiveCharacter

noncomputable def primeSumOver (S : Set Nat.Primes) (s : ℝ) : ℝ

noncomputable def primeSumAll (s : ℝ) : ℝ

noncomputable def dirichletDensityRatio (S : Set Nat.Primes) (s : ℝ) : ℝ

def HasDirichletDensity (S : Set Nat.Primes) (d : ℝ) : Prop

noncomputable def dirichletDensity (S : Set Nat.Primes) : ℝ