Theorem Matrix.linearIndependent_col_of_invertible

Modification history

2026-09-30 15:24

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

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

Added Matrix.linearIndependent_col_of_invertible View on Github →