toQuadraticMap_list_sum — Mathlib

English

For a finite list of BilinMap, the sum of their 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_list_sum (B : List (BilinMap R M N)) : B.sum.toQuadraticMap = (B.map toQuadraticMap).sum :=
  map_list_sum (toQuadraticMapAddMonoidHom R M) B

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