Commit 2025-07-15 08:11 11385264

View on Github →

refactor(LinearAlgebra/LinearIndependent): generalize some LinearIndepOn theorems (#27096) A lot of APIs and theorems for LinearIndepOn are stated only for id. This PR tries to generalize some of them to be non id, keeping the old id APIs as special cases.

Estimated changes

Modified Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

modified theorem LinearIndepOn.extend_subset

added theorem LinearIndepOn.image_subset_span_image_extend

modified theorem LinearIndepOn.linearIndepOn_extend

modified theorem LinearIndepOn.span_extend_eq_span

added theorem LinearIndepOn.span_image_extend_eq_span_image

modified theorem LinearIndepOn.subset_extend

modified theorem LinearIndepOn.subset_span_extend

modified theorem exists_finite_card_le_of_finite_of_linearIndependent_of_span

added theorem exists_linearIndepOn_extension

modified theorem exists_of_linearIndepOn_of_finite_span