Theorem Matrix.IsReducedRowEchelon.eq_zero_of_ne_of_isLeadingEntry

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.eq_zero_of_ne_of_isLeadingEntryView on Github →