Theorem exists_linearIndependent'

Modification history

2025-02-25 23:58
Mathlib/LinearAlgebra/LinearIndependent.lean
chore(LinearAlgebra): split LinearIndependent into Defs, Basic, Lemmas (#22065) …
Modified exists_linearIndependent'View on Github →
2024-12-27 19:18
Mathlib/LinearAlgebra/LinearIndependent.lean
chore(RingTheory/LocalRing): strengthen `Module.free_of_flat_of_isLocalRing` (#19846) …
Added exists_linearIndependent'View on Github →