theorem CharacterOrthogonality.orthogonality_group {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (g₁ g₂ : G) : ∑ χ : AddChar G ℂ, χ g₁ * (starRingEnd ℂ) (χ g₂) = if g₁ = g₂ then ↑(Fintype.card G) else 0

theorem CharacterOrthogonality.orthogonality_group_normalized {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (g₁ g₂ : G) : (↑(Fintype.card G))⁻¹ * ∑ χ : AddChar G ℂ, χ g₁ * (starRingEnd ℂ) (χ g₂) = if g₁ = g₂ then 1 else 0

theorem CharacterOrthogonality.orthogonality_char {G : Type u_1} [AddCommGroup G] [Fintype G] (χ₁ χ₂ : AddChar G ℂ) : ∑ g : G, χ₁ g * (starRingEnd ℂ) (χ₂ g) = if χ₁ = χ₂ then ↑(Fintype.card G) else 0

theorem CharacterOrthogonality.orthogonality_char_normalized {G : Type u_1} [AddCommGroup G] [Fintype G] (χ₁ χ₂ : AddChar G ℂ) : (↑(Fintype.card G))⁻¹ * ∑ g : G, χ₁ g * (starRingEnd ℂ) (χ₂ g) = if χ₁ = χ₂ then 1 else 0

theorem CharacterOrthogonality.character_orthogonality_relations {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] : (∀ (g₁ g₂ : G), (↑(Fintype.card G))⁻¹ * ∑ χ : AddChar G ℂ, χ g₁ * (starRingEnd ℂ) (χ g₂) = if g₁ = g₂ then 1 else 0) ∧ ∀ (χ₁ χ₂ : AddChar G ℂ), (↑(Fintype.card G))⁻¹ * ∑ g : G, χ₁ g * (starRingEnd ℂ) (χ₂ g) = if χ₁ = χ₂ then 1 else 0