Commit 2025-02-14 22:50 ba17ac8c

chore(Data/Finset): don't import algebra in Finset.Lattice.Fold (#21883) We don't need to know what a monoid is in order to define the maximum of a finset. This PR replaces the approach of #21874 (reversing the Finset.Max -> Finset.Sort import) with cleaning up Finset.Max's dependencies. In particular, we reverse the import direction for Multiset.Bind and Multiset.Fold (the former imports a lot anyway), and split some results off from Finset.Lattice.Fold based on dependencies: Finset.{Pi,Prod,Union} mapping to Finset.Lattice.{Pi,Prod,Union}.