Standard basis on matrices

Main results

• Basis.matrix: extend a basis on M to the standard basis on Matrix n m M

noncomputable def Module.Basis.matrix {ι : Type u_1} {R : Type u_2} {M : Type u_3} (m : Type u_4) (n : Type u_5) [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : Basis (m × n × ι) R (Matrix m n M)

The standard basis of Matrix m n M given a basis on M.

@[simp]

theorem Module.Basis.matrix_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {m : Type u_4} {n : Type u_5} [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : m) (j : n) (k : ι) [DecidableEq m] [DecidableEq n] : (Basis.matrix m n b) (i, j, k) = Matrix.single i j (b k)

noncomputable def Matrix.stdBasis (R : Type u_1) (m : Type u_2) (n : Type u_3) [Fintype m] [Finite n] [Semiring R] : Module.Basis (m × n) R (Matrix m n R)

The standard basis of Matrix m n R.

theorem Matrix.stdBasis_eq_single (R : Type u_1) {m : Type u_2} {n : Type u_3} [Fintype m] [Finite n] [Semiring R] (i : m) (j : n) [DecidableEq m] [DecidableEq n] : (stdBasis R m n) (i, j) = single i j 1

instance Module.Free.matrix (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] {m : Type u_3} {n : Type u_4} [Finite m] [Finite n] : Free R (Matrix m n M)

The module of finite matrices is free.