toMatrix' — Mathlib

English

The linear equivalence between BilinForm on n×n and matrices is implemented by toMatrix'.

Русский

Линейное эквивалентное отображение между билинейными формами и матрицами реализуется через toMatrix'.

LaTeX

$$$\text{toMatrix'} \colon BilinForm R (n \to R) \simeq \mathrm{Matrix}_{n,n}R$$$

Lean4

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

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