ZModCircle.lean

theorem exists_toAddCircle_eq_of_nsmul_eq_zero
    (N : ℕ) [NeZero N] (z : UnitAddCircle) (hz : N • z = 0) :
    ∃ a : ZMod N, toAddCircle a = z

theorem toAddCircle_castHom_mul
    (N m : ℕ) [NeZero N] [NeZero m] (a : ZMod (N * m)) :
    toAddCircle (castHom (dvd_mul_right N m) (ZMod N) a) =
      m • toAddCircle a

theorem exists_continuous_zmod_character
    {A : Type*} [Group A] [TopologicalSpace A]
    (N : ℕ) [NeZero N] (f : A →ₜ* Multiplicative UnitAddCircle)
    (hf : ∀ a : A, N • (f a).toAdd = 0) :
    ∃ g : A →ₜ* Multiplicative (ZMod N), ∀ a : A,
      toAddCircle (g a).toAdd = (f a).toAdd