toMvPolynomial_add — Mathlib

English

For linear maps f and g, (f + g).toMvPolynomial b1 b2 = f.toMvPolynomial b1 b2 + g.toMvPolynomial b1 b2.

Русский

Для линейных отображений f и g выполняется (f+g).toMvPolynomial b1 b2 = f.toMvPolynomial b1 b2 + g.toMvPolynomial b1 b2.

LaTeX

$$(f + g).toMvPolynomial b1 b2 = f.toMvPolynomial b1 b2 + g.toMvPolynomial b1 b2$$

Lean4

theorem toMvPolynomial_add (f g : M₁ →ₗ[R] M₂) :
    (f + g).toMvPolynomial b₁ b₂ = f.toMvPolynomial b₁ b₂ + g.toMvPolynomial b₁ b₂ := by unfold toMvPolynomial;
  simp only [map_add, Matrix.toMvPolynomial_add]

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