toMatrix_toBilin — Mathlib

English

Applying Matrix.toBilin to bilinear form represented by a matrix returns the original bilinear form.

Русский

Применение Matrix.toBilin к билинейной форме, представленой матрицей, возвращает исходную билинейную форму.

LaTeX

$$BilinForm.toMatrix b (Matrix.toBilin b M) = M$$

Lean4

@[simp]
theorem toMatrix_toBilin (M : Matrix n n R₁) : BilinForm.toMatrix b (Matrix.toBilin b M) = M :=
  (BilinForm.toMatrix b).apply_symm_apply M

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