Theorem Matrix.stdBasisMatrix_add

Modification history

2024-10-25 13:43

Mathlib/Data/Matrix/Basis.lean

feat: Matrices over finite free modules are finite modules (#18098) …

Modified Matrix.stdBasisMatrix_add View on Github →

2023-04-04 13:03

Mathlib/Data/Matrix/Basis.lean

feat: port Data.Matrix.Basis (#3243)

Added Matrix.stdBasisMatrix_add View on Github →