toQuadraticMap_apply — Mathlib

English

For BilinMap B and f: N' →ₗ[R] M, BilinMap.toQuadraticMap (B.compl₁₂ f f) equals B.toQuadraticMap.comp f.

Русский

Для билинейного отображения B и линейного отображения f: N' →ₗ[R] M, BilinMap.toQuadraticMap (B.compl₁₂ f f) равно B.toQuadraticMap.comp f.

LaTeX

$$$B\!:\! BilinMap\ R\ M\ N$, $f:\! N' \to M$, then $B_{compl} (f,f)\toQuadraticMap = B.toQuadraticMap . comp f$.$$

Lean4

@[simp]
theorem toQuadraticMap_apply (B : BilinMap R M N) (x : M) : B.toQuadraticMap x = B x x :=
  rfl

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