toQuadraticMap_comp_same — Mathlib

English

Same as above: the quadratic map of a composed bilinear map matches composition with f.

Русский

То же самое: квадратичное отображение от составленного билинейного отображения совпадает с композиции с f.

LaTeX

$$$B.compl_12 f f \mapsto B.toQuadraticMap . comp f$$$

Lean4

theorem toQuadraticMap_comp_same (B : BilinMap R M N) (f : N' →ₗ[R] M) :
    BilinMap.toQuadraticMap (B.compl₁₂ f f) = B.toQuadraticMap.comp f :=
  rfl

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