Theorem Matrix.linearIndependent_cols_iff_isUnit

Modification history

2026-09-30 15:24

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

chore(LinearAlgebra/Matrix/NonsingularInverse): generalize some lemmas from `Field` to `IsArtinianRing` (#44054) …

Deleted Matrix.linearIndependent_cols_iff_isUnit View on Github →

2023-12-08 12:43

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

feat: Invertible matrices (#8219) …

Added Matrix.linearIndependent_cols_iff_isUnit View on Github →