Commit 2025-03-07 22:53 7590675d

chore(LinearAlgebra): split long file Dual.lean (#22697) This PR splits LinearAlgebra.Dual into three new files:

• Dual/Defs.lean: definition of dual vector spaces and basic operations
• Dual/Basis.lean: defines a basis on the dual space
• Dual/Lemmas.lean: lemmas about dual spaces It would be nice if we could split Lemmas.lean further, but it looks like we just have a huge chunk importing FiniteDimensional and then a few random lemmas with extra imports; we'd need to untangle that bit of the library further before we'd start seeing actual import improvements. (Hint for bored reviewers: #22593, #22693)