toMatrix'_symm — Mathlib

English

The symmetry of the bilinear-to-matrix equivalence is given by toMatrix'_symm: the inverse of toMatrix' is BilinForm.toMatrix'.

Русский

Симметричность перехода между билинейной формой и матрицей: toMatrix'_symm — обратная к toMatrix'.

LaTeX

$$$\text{toMatrix'}\_symm : (toMatrix' \text{ symm}) = \text{BilinForm.toMatrix'}$$$

Lean4

@[simp]
theorem toMatrix'_symm : (BilinForm.toMatrix'.symm : Matrix n n R₁ ≃ₗ[R₁] _) = Matrix.toBilin' :=
  rfl

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