Theorem LinearIndepOn.image_subset_span_image_extend

Modification history

2025-07-15 08:11
Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
refactor(LinearAlgebra/LinearIndependent): generalize some `LinearIndepOn` theorems (#27096) …
Added LinearIndepOn.image_subset_span_image_extendView on Github →