Theorem LinearIndependent.of_subsingleton

Modification history

2025-11-12 09:50
Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
feat: add an element to a linear indep family, more general version (#31515)
Added LinearIndependent.of_subsingletonView on Github →