Commit 2026-09-30 15:24 69452e24

View on Github →

chore(LinearAlgebra/Matrix/NonsingularInverse): generalize some lemmas from Field to IsArtinianRing (#44054) ... also fix their names.

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

added theorem Matrix.linearIndependent_col_iff_isUnit

added theorem Matrix.linearIndependent_col_of_invertible

deleted theorem Matrix.linearIndependent_cols_iff_isUnit

deleted theorem Matrix.linearIndependent_cols_of_invertible

added theorem Matrix.linearIndependent_row_iff_isUnit

added theorem Matrix.linearIndependent_row_of_invertible

deleted theorem Matrix.linearIndependent_rows_iff_isUnit

deleted theorem Matrix.linearIndependent_rows_of_invertible