TODO

Rename

• map_add_mul → map_add_eq_mul
• map_zero_one → map_zero_eq_one
• map_nsmul_pow → map_nsmul_eq_pow

@[simp]

theorem AddChar.norm_apply {G : Type u_1} {R : Type u_3} [AddGroup G] [Finite G] [NormedField R] (ψ : AddChar G R) (x : G) : ‖ψ x‖ = 1

@[simp]

theorem AddChar.coe_ne_zero {G : Type u_1} {R : Type u_3} [AddGroup G] [NormedField R] (ψ : AddChar G R) : ⇑ψ ≠ 0

theorem AddChar.inv_apply_eq_conj {G : Type u_1} {R : Type u_3} [AddGroup G] [RCLike R] [Finite G] (ψ : AddChar G R) (x : G) : (ψ x)⁻¹ = (starRingEnd R) (ψ x)

theorem AddChar.l2Inner_self {G : Type u_1} {R : Type u_3} [AddGroup G] [RCLike R] [Fintype G] (ψ : AddChar G R) : l2Inner ⇑ψ ⇑ψ = ↑(Fintype.card G)

theorem AddChar.expect_eq_ite {G : Type u_1} {R : Type u_3} [AddGroup G] [Fintype G] [Semifield R] [IsDomain R] [CharZero R] (ψ : AddChar G R) : (Finset.expect Finset.univ 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_3} [AddGroup G] [Fintype G] [Semifield R] [IsDomain R] [CharZero R] {ψ : AddChar G R} : (Finset.expect Finset.univ fun (x : G) => ψ x) = 0 ↔ ψ ≠ 0

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

theorem AddChar.map_neg_eq_conj {G : Type u_1} {R : Type u_3} [AddCommGroup G] [RCLike R] [Finite G] (ψ : AddChar G R) (x : G) : ψ (-x) = (starRingEnd R) (ψ x)

theorem AddChar.l2Inner_eq {G : Type u_1} {R : Type u_3} [AddCommGroup G] [RCLike R] [Fintype G] (ψ₁ : AddChar G R) (ψ₂ : AddChar G R) : l2Inner ⇑ψ₁ ⇑ψ₂ = if ψ₁ = ψ₂ then ↑(Fintype.card G) else 0

theorem AddChar.l2Inner_eq_zero_iff_ne {G : Type u_1} {R : Type u_3} [AddCommGroup G] [RCLike R] {ψ₁ : AddChar G R} {ψ₂ : AddChar G R} [Fintype G] : l2Inner ⇑ψ₁ ⇑ψ₂ = 0 ↔ ψ₁ ≠ ψ₂

theorem AddChar.l2Inner_eq_card_iff_eq {G : Type u_1} {R : Type u_3} [AddCommGroup G] [RCLike R] {ψ₁ : AddChar G R} {ψ₂ : AddChar G R} [Fintype G] : l2Inner ⇑ψ₁ ⇑ψ₂ = ↑(Fintype.card G) ↔ ψ₁ = ψ₂

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

noncomputable instance AddChar.instFintype (G : Type u_1) (R : Type u_3) [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_3) [AddCommGroup G] [RCLike R] [Fintype G] : Fintype.card (AddChar G R) ≤ Fintype.card G

def AddChar.directSum {R : Type u_3} {ι : Type u_4} {π : ι → Type u_5} [DecidableEq ι] [(i : ι) → AddCommGroup (π i)] [CommMonoid R] (ψ : (i : ι) → AddChar (π i) R) : AddChar (DirectSum ι fun (i : ι) => π i) R

Direct sum of additive characters.

Equations

• AddChar.directSum ψ = AddChar.toAddMonoidHomEquiv'.symm (DirectSum.toAddMonoid fun (i : ι) => AddChar.toAddMonoidHomEquiv' (ψ i))

theorem AddChar.directSum_injective {R : Type u_3} {ι : Type u_4} {π : ι → Type u_5} [DecidableEq ι] [(i : ι) → AddCommGroup (π i)] [CommMonoid R] : Function.Injective AddChar.directSum