toMatrix'_toBilin' — Mathlib

English

The matrix-to-bilinear-form correspondence and the bilinear-form-to-matrix correspondence are inverse to each other; applying Matrix.toBilin' followed by BilinForm.toMatrix' yields the original matrix.

Русский

Соответствие между матрицей и билинейной формой образует взаимно обратную пару; применение Matrix.toBilin' затем BilinForm.toMatrix' возвращает исходную матрицу.

LaTeX

$$$\operatorname{toMatrix'}\big(\operatorname{Matrix.toBilin'}(M)\big) = M$$$

Lean4

@[simp]
theorem toMatrix'_toBilin' (M : Matrix n n R₁) : BilinForm.toMatrix' (Matrix.toBilin' M) = M :=
  (LinearMap.toMatrix₂' R₁).apply_symm_apply M

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