toMvPolynomial_add — Mathlib

English

The map toMvPolynomial is additive in the matrix: (M + N).toMvPolynomial i = M.toMvPolynomial i + N.toMvPolynomial i.

Русский

Отображение toMvPolynomial линейно по матрицам: (M + N).toMvPolynomial i = M.toMvPolynomial i + N.toMvPolynomial i.

LaTeX

$$(M + N).toMvPolynomial i = M.toMvPolynomial i + N.toMvPolynomial i$$

Lean4

theorem toMvPolynomial_add (M N : Matrix m n R) : (M + N).toMvPolynomial = M.toMvPolynomial + N.toMvPolynomial :=
  by
  ext i : 1
  simp only [toMvPolynomial, add_apply, map_add, Finset.sum_add_distrib, Pi.add_apply]

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