theorem lem_18_12 {m : ℕ} [NeZero m] (χ : DirichletCharacter ℂ m) : ∑ n : ZMod m, χ n ≠ 0 ↔ χ = 1