Commit 2025-02-14 22:50 ba17ac8c
View on Github →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}
.