Commit 2025-02-25 23:58 c28c3dab

chore(LinearAlgebra): split LinearIndependent into Defs, Basic, Lemmas (#22065) I was looking at reducing the imports and non-deffiness of LinearAlgebra.Basis.Defs and one big obstacle is that the basic dependencies in linear algebra already bring in a lot of theory. So I decided to try and split this large file. I ended up with three files:

• LinearIndependent.Defs contains the definitions and lemmas stating equivalent definitions to linear independence.
• LinearIndependent.Basic contains results provable without additional imports
• LinearIndependent.Lemmas contains the rest of the lemmas