toQuadraticMap_add — Mathlib

English

The mapping toQuadraticMap is additive: (B1 + B2).toQuadraticMap = B1.toQuadraticMap + B2.toQuadraticMap.

Русский

Отображение в квадратичное отображение аддитивно: (B1 + B2).toQuadraticMap = B1.toQuadraticMap + B2.toQuadraticMap.

LaTeX

$$$ (B_1 + B_2).toQuadraticMap = B_1.toQuadraticMap + B_2.toQuadraticMap $$$

Lean4

@[simp]
theorem toQuadraticMap_add (B₁ B₂ : BilinMap R M N) :
    (B₁ + B₂).toQuadraticMap = B₁.toQuadraticMap + B₂.toQuadraticMap :=
  rfl

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