Theorem Matrix.det_eq_zero_of_not_linearIndependent_rows

Modification history

2025-05-23 17:11
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
feat(NumberField/Units): add `regOfFamily` and refactor `regulator` (#22882) …
Added Matrix.det_eq_zero_of_not_linearIndependent_rowsView on Github →