toLinearMapₛₗ₂' — Mathlib

English

A matrix is determined by its entries on basis delta vectors: M_{ij} = f(e_i,e_j).

Русский

Матрица задаётся своими элементами на базисе: M_{ij} = f(e_i,e_j).

LaTeX

$$$M_{ij} = f(e_i,e_j)$$$

Lean4

/-- The linear equivalence between `n × n` matrices and sesquilinear maps on `n → R` -/
def toLinearMapₛₗ₂' : Matrix n m N₂ ≃ₗ[R] (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂ :=
  (LinearMap.toMatrixₛₗ₂' R).symm

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