Mathlib Changelog
v4
Changelog
About
Github
Theorem
LinearIndepOn.span_image_extend_eq_span_image
Modification history
2025-07-15 08:11
Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
refactor(LinearAlgebra/LinearIndependent): generalize some `LinearIndepOn` theorems (#27096) …
Added
LinearIndepOn.span_image_extend_eq_span_image
View on Github →