Theorem Matrix.linearIndependent_rows_of_isUnit

Modification history

2025-08-19 02:03
Mathlib/LinearAlgebra/Matrix/ToLin.lean
feat(Data/Matrix): relax some `IsUnit` lemmas to `IsRegular` (#28500) …
Modified Matrix.linearIndependent_rows_of_isUnitView on Github →
2025-03-20 16:17
Mathlib/LinearAlgebra/Matrix/ToLin.lean
feat: generalize Mathlib.LinearAlgebra.Matrix (#23144) …
Modified Matrix.linearIndependent_rows_of_isUnitView on Github →
2025-01-09 15:53
Mathlib/LinearAlgebra/Matrix/ToLin.lean
feat(RingTheory/StandardSmooth): pre-requisites for calculating the naive cotangent complex of a submersive presentation (#19749) …
Added Matrix.linearIndependent_rows_of_isUnitView on Github →