toQuadraticMap_multiset_sum — Mathlib

English

For a multiset of BilinMap, the sum of their quadratic maps equals the quadratic map of the multiset's sum.

Русский

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

LaTeX

$$$B.sum.toQuadraticMap = (B.map toQuadraticMap).sum$ for multiset B.$$

Lean4

@[simp]
theorem toQuadraticMap_multiset_sum (B : Multiset (BilinMap R M N)) :
    B.sum.toQuadraticMap = (B.map toQuadraticMap).sum :=
  map_multiset_sum (toQuadraticMapAddMonoidHom R M) B

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