Commit 2025-03-10 16:50 261ed584

chore(Algebra/BigOperators): reverse Finsupp <-> Fin import direction (#22770) This was spotted while looking at the files depending on Data.Finset.Image and Data.Finset.Fin. By reversing the import order between BigOperators.Finsupp and BigOperators.Fin we can avoid importing a lot of work on Fin that we don't need. Especially in linear algebra and related topics that import saves a bit. On the other hand, some files do have their import graph grow a bit. But I think the tradeoff is definitely worth it. And moreover, it makes a follow-up PR moving Finset.fin downstream from Data.Finset.Image to Data.Finset.Fin work a bit better.