toQuadraticMap_sum — Mathlib

English

For a finite index set, the sum of BilinMap's quadratic maps equals the quadratic map of the sum.

Русский

Для конечного множества индексов сумма квадратичных отображений BilinMap равна квадратичному отображению суммы.

LaTeX

$$$\sum_{i} B_i .toQuadraticMap = (\sum_{i} B_i).toQuadraticMap$$$

Lean4

@[simp]
theorem toQuadraticMap_sum {ι : Type*} (s : Finset ι) (B : ι → (BilinMap R M N)) :
    (∑ i ∈ s, B i).toQuadraticMap = ∑ i ∈ s, (B i).toQuadraticMap :=
  map_sum (toQuadraticMapAddMonoidHom R M) B s

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