English
The standard basis of the matrix space M_{m×n}(M) is obtained from a given basis on M by arranging basis elements into matrix form.
Русский
Стандартный базис пространства матриц M_{m×n}(M) получаем из заданного базиса на M, упорядочив базисные элементы в матричную форму.
LaTeX
$$$\\text{Basis}_{m\\times n}(M) \\sim \\text{Matrix}$$$$
Lean4
/-- The standard basis of `Matrix m n M` given a basis on `M`. -/
protected noncomputable def matrix (b : Basis ι R M) : Basis (m × n × ι) R (Matrix m n M) :=
Basis.reindex (Pi.basis fun _ : m => Pi.basis fun _ : n => b)
((Equiv.sigmaEquivProd _ _).trans <| .prodCongr (.refl _) (Equiv.sigmaEquivProd _ _)) |>.map
(Matrix.ofLinearEquiv R)
