Theorem Matrix.linearIndependent_col_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) …

Added Matrix.linearIndependent_col_iff_isUnit View on Github →