toQuadraticMap_sub — Mathlib

English

Let B1 and B2 be bilinear maps. The quadratic map associated to their difference equals the difference of their quadratic maps:

Русский

Пусть B1 и B2 — билинейные отображения. Соответствующая квадратичная карта к их разности равна разности соответствующих квадратичных карт:

LaTeX

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

Lean4

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

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