theorem CharacterOrthogonality.sum_char_ne_zero_iff {G : Type u_1} [AddCommGroup G] [Fintype G] (χ : AddChar G ℂ) : ∑ g : G, χ g ≠ 0 ↔ χ = 0

theorem CharacterOrthogonality.sum_dual_ne_zero_iff {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (g : G) : ∑ χ : AddChar G ℂ, χ g ≠ 0 ↔ g = 0

theorem CharacterOrthogonality.corollary_18_38 {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] : (∀ (χ : AddChar G ℂ), ∑ g : G, χ g ≠ 0 ↔ χ = 0) ∧ ∀ (g : G), ∑ χ : AddChar G ℂ, χ g ≠ 0 ↔ g = 0