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