sum_eq_card_of_eq_one — Mathlib

English

If ψ is the trivial additive character, the sum over a ∈ R of ψ(a) equals |R|.

Русский

Если ψ тривиальная аддитивная характеристика, то сумма по a ∈ R ψ(a) равна кардинальности R.

LaTeX

$$∑_{a∈R} ψ(a) = |R|$$

Lean4

/-- The sum over the values of the trivial additive character is the cardinality of the source. -/
theorem sum_eq_card_of_eq_one {ψ : AddChar R R'} (hψ : ψ = 1) : ∑ a, ψ a = Fintype.card R := by simp [hψ]

Похожие утверждения