Theorem exists_finite_card_le_of_finite_of_linearIndependent_of_span
Modification history
2025-07-15 08:11
Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
refactor(LinearAlgebra/LinearIndependent): generalize some `LinearIndepOn` theorems (#27096) …
Modified exists_finite_card_le_of_finite_of_linearIndependent_of_spanView on Github →