Theorem linearIndepOn_iff_not_mem_span

Modification history

2025-05-25 12:30
Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
chore(*): not_mem/nmem -> notMem (#25159)
Deleted linearIndepOn_iff_not_mem_spanView on Github →
2025-03-18 05:39
Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
feat: `LinearIndepOn K v s ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))` (#22874) …
Added linearIndepOn_iff_not_mem_spanView on Github →