toBilin'_apply' — Mathlib

English

The explicit expansion of the bilinear form associated to a matrix is the dot product expression with M.

Русский

Явное разложение билинейной формы, ассоциированной с матрицей, через скалярное произведение.

LaTeX

$$$\text{toBilin'}\_apply'(M,x,y) = \,x \cdot (M \cdot y)$$$

Lean4

theorem toBilin'_apply' (M : Matrix n n R₁) (v w : n → R₁) : Matrix.toBilin' M v w = v ⬝ᵥ M *ᵥ w :=
  Matrix.toLinearMap₂'_apply' _ _ _

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