Structure Matrix.IsReducedRowEchelon

Modification history

2026-07-30 16:24

Mathlib/LinearAlgebra/Matrix/Echelon/Basic.lean

feat(LinearAlgebra/Matrix): add definitions and theory for the echelon form and pivots of matrices (#42236) …

Added Matrix.IsReducedRowEchelon View on Github →