structure PrimCharDvd (R : Type u_1) [CommMonoidWithZero R] (m : ℕ) : Type u_1

• d : ℕ
• hdvd : self.d ∣ m
• χ : DirichletCharacter R self.d
• hprim : self.χ.IsPrimitive

theorem PrimCharDvd.ext' {R : Type u_1} [CommMonoidWithZero R] {m : ℕ} {p q : PrimCharDvd R m} (hd : p.d = q.d) (hχ : hd ▸ p.χ = q.χ) : p = q

theorem DirichletCharacter.changeLevel_cast_eq {R : Type u_1} [CommMonoidWithZero R] {m d₁ d₂ : ℕ} (heq : d₁ = d₂) (hd₂ : d₂ ∣ m) (ψ : DirichletCharacter R d₁) : (changeLevel hd₂) (heq ▸ ψ) = (changeLevel ⋯) ψ

noncomputable def DirichletCharacter.toPrimCharDvd {R : Type u_1} [CommMonoidWithZero R] {m : ℕ} (χ : DirichletCharacter R m) : PrimCharDvd R m

noncomputable def DirichletCharacter.fromPrimCharDvd {R : Type u_1} [CommMonoidWithZero R] {m : ℕ} (p : PrimCharDvd R m) : DirichletCharacter R m

theorem DirichletCharacter.fromPrimCharDvd_toPrimCharDvd {R : Type u_1} [CommMonoidWithZero R] {m : ℕ} (χ : DirichletCharacter R m) : fromPrimCharDvd χ.toPrimCharDvd = χ

theorem DirichletCharacter.conductor_changeLevel_of_isPrimitive {R : Type u_1} [CommMonoidWithZero R] {m d : ℕ} (hm : m ≠ 0) (hd : d ∣ m) (ψ : DirichletCharacter R d) (hprim : ψ.IsPrimitive) : ((changeLevel hd) ψ).conductor = d

theorem DirichletCharacter.toPrimCharDvd_fromPrimCharDvd {R : Type u_1} [CommMonoidWithZero R] {m : ℕ} (hm : m ≠ 0) (p : PrimCharDvd R m) : (fromPrimCharDvd p).toPrimCharDvd = p

noncomputable def DirichletCharacter.cor_18_16_M_equivMul_Ghat {R : Type u_1} [CommMonoidWithZero R] (m : ℕ) : DirichletCharacter R m ≃* ((ZMod m)ˣ →* Rˣ)

noncomputable def DirichletCharacter.cor_18_16_M_equiv_X {R : Type u_1} [CommMonoidWithZero R] (m : ℕ) (hm : m ≠ 0) : DirichletCharacter R m ≃ PrimCharDvd R m