toBilin' — Mathlib

English

The twofold equivalence between BilinForm and Matrix commute with identity isomorphisms.

Русский

Две эквивалентности между BilinForm и Matrix совместимы с единичными изоморфизмами.

LaTeX

$$$\text{toBilin'_eq}$$$

Lean4

/-- The linear equivalence between `n × n` matrices and bilinear forms on `n → R` -/
def toBilin' : Matrix n n R₁ ≃ₗ[R₁] BilinForm R₁ (n → R₁) :=
  BilinForm.toMatrix'.symm

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