English
For primitive ψ and b ∈ R, the sum ∑_{x∈R} ψ(x b) equals |R| if b = 0, otherwise 0.
Русский
Для примитивной ψ и любого b ∈ R сумма ∑ ψ(x b) равна |R|, если b = 0, иначе 0.
LaTeX
$$∑_{x∈R} ψ(x b) = if b = 0 then card R else 0$$
Lean4
/-- The sum over the values of `mulShift ψ b` for `ψ` primitive is zero when `b ≠ 0`
and `#R` otherwise. -/
theorem sum_mulShift {R : Type*} [CommRing R] [Fintype R] [DecidableEq R] {R' : Type*} [CommRing R'] [IsDomain R']
{ψ : AddChar R R'} (b : R) (hψ : IsPrimitive ψ) : ∑ x : R, ψ (x * b) = if b = 0 then Fintype.card R else 0 :=
by
split_ifs with h
· -- case `b = 0`
simp only [h, mul_zero, map_zero_eq_one, Finset.sum_const, Nat.smul_one_eq_cast]
rfl
· -- case `b ≠ 0`
simp_rw [mul_comm]
exact mod_cast sum_eq_zero_of_ne_one (hψ h)
