Theorem exists_linearIndepOn_extension

Modification history

2025-07-15 08:11

Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

refactor(LinearAlgebra/LinearIndependent): generalize some `LinearIndepOn` theorems (#27096) …

Added exists_linearIndepOn_extension View on Github →