stdBasis — Mathlib

English

The standard basis for Matrix m n R is a Basis for the space of matrices.

Русский

Стандартный базис для пространства матриц M_{m×n}(R) образует базис этого пространства.

LaTeX

$$$\\\\text{stdBasis} :\\\\ Basis \\\\,(m\\\\times n) \\\\ R \\\\ (Matrix m n R)$$$

Lean4

/-- The standard basis of `Matrix m n R`. -/
noncomputable def stdBasis : Basis (m × n) R (Matrix m n R) :=
  Basis.reindex (Pi.basis fun _ : m => Pi.basisFun R n) (Equiv.sigmaEquivProd _ _) |>.map (ofLinearEquiv R)

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