Commit 2025-03-17 19:11 cd146f39

chore(LinearAlgebra/FiniteDimensional): rearrange Defs.lean (#22593) We have two files named after finite dimensional vector spaces:

• LinearAlgebra/FiniteDimensional/Defs.lean (definition and lemmas)
• LinearAlgebra/FiniteDimensional.lean (more lemmas) This PR rearranges the files into three:
• LinearAlgebra/FiniteDimensional/Defs.lean (definition, equivalence between Module.Finite, IsNoetherian and existence of a fintype basis)
• LinearAlgebra/FiniteDimensional/Basic.lean (basic results, moved from Defs.lean)
• LinearAlgebra/FiniteDimensional/Lemmas.lean (more lemmas) The whole finiteness hierarchy is still quite a mess, but at least this bit is a bit neater now.