Orthogonality of characters of a finite abelian group

This file proves that characters of a finite abelian group are orthogonal, and in particular that there are at most as many characters as there are elements of the group.

theorem AddChar.expect_eq_ite {G : Type u_1} {R : Type u_2} [AddGroup G] [Fintype G] [Semifield R] [CharZero R] (ψ : AddChar G R) : (Finset.univ.expect fun (a : G) => ψ a) = if ψ = 0 then 1 else 0

theorem AddChar.expect_eq_zero_iff_ne_zero {G : Type u_1} {R : Type u_2} [AddGroup G] [Fintype G] [Semifield R] [CharZero R] {ψ : AddChar G R} : (Finset.univ.expect fun (x : G) => ψ x) = 0 ↔ ψ ≠ 0

theorem AddChar.expect_ne_zero_iff_eq_zero {G : Type u_1} {R : Type u_2} [AddGroup G] [Fintype G] [Semifield R] [CharZero R] {ψ : AddChar G R} : (Finset.univ.expect fun (x : G) => ψ x) ≠ 0 ↔ ψ = 0

theorem AddChar.wInner_cWeight_self {G : Type u_1} {R : Type u_2} [AddGroup G] [RCLike R] [Fintype G] (ψ : AddChar G R) : ⟪⇑ψ, ⇑ψ⟫ₙ_[R] = 1

theorem AddChar.wInner_cWeight_eq_boole {G : Type u_1} {R : Type u_2} [AddCommGroup G] [RCLike R] [Fintype G] (ψ₁ ψ₂ : AddChar G R) : ⟪⇑ψ₁, ⇑ψ₂⟫ₙ_[R] = if ψ₁ = ψ₂ then 1 else 0

theorem AddChar.wInner_cWeight_eq_zero_iff_ne {G : Type u_1} {R : Type u_2} [AddCommGroup G] [RCLike R] {ψ₁ ψ₂ : AddChar G R} [Fintype G] : ⟪⇑ψ₁, ⇑ψ₂⟫ₙ_[R] = 0 ↔ ψ₁ ≠ ψ₂

theorem AddChar.wInner_cWeight_eq_one_iff_eq {G : Type u_1} {R : Type u_2} [AddCommGroup G] [RCLike R] {ψ₁ ψ₂ : AddChar G R} [Fintype G] : ⟪⇑ψ₁, ⇑ψ₂⟫ₙ_[R] = 1 ↔ ψ₁ = ψ₂

theorem AddChar.linearIndependent (G : Type u_1) (R : Type u_2) [AddCommGroup G] [RCLike R] [Finite G] : LinearIndependent R DFunLike.coe

@[instance_reducible]

noncomputable instance AddChar.instFintype (G : Type u_1) (R : Type u_2) [AddCommGroup G] [RCLike R] [Finite G] : Fintype (AddChar G R)

Equations

• AddChar.instFintype G R = Fintype.ofFinite (AddChar G R)

@[simp]

theorem AddChar.card_addChar_le (G : Type u_1) (R : Type u_2) [AddCommGroup G] [RCLike R] [Fintype G] : Fintype.card (AddChar G R) ≤ Fintype.card G