toBilin'_symm — Mathlib

English

The symmetry of the matrix-to-bilin equivalence is captured by toBilin'_symm: (Matrix.toBilin'.symm) = BilinForm.toMatrix'.

Русский

Симметричность связи между Matrix и BilinForm выражается через toBilin'_symm: (Matrix.toBilin'.symm) = BilinForm.toMatrix'.

LaTeX

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

Lean4

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

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