sum_apply — Mathlib

English

The sum of a finite family of quadratic maps is again a quadratic map; its evaluation is the sum of evaluations.

Русский

Сумма конечной семейства квадратичных отображений образует квадратичную карту; значение суммы равно сумме значений.

LaTeX

$$$\\big( \\sum_{i\\in s} Q_i \\big)(x) = \\sum_{i\\in s} Q_i(x)$ for all x and finite s.$$

Lean4

@[simp]
theorem sum_apply {ι : Type*} (Q : ι → QuadraticMap R M N) (s : Finset ι) (x : M) : (∑ i ∈ s, Q i) x = ∑ i ∈ s, Q i x :=
  map_sum (evalAddMonoidHom x : _ →+ N) Q s

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