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}.

Estimated changes

deleted theorem Finset.inf'_biUnion
deleted theorem Finset.inf'_prodMap
deleted theorem Finset.inf'_product_left
deleted theorem Finset.inf'_product_right
deleted theorem Finset.inf'_sup_inf'
deleted theorem Finset.inf_biUnion
deleted theorem Finset.inf_prodMap
deleted theorem Finset.inf_product_left
deleted theorem Finset.inf_product_right
deleted theorem Finset.inf_sup
deleted theorem Finset.inf_sup_inf
deleted theorem Finset.prodMk_inf'_inf'
deleted theorem Finset.prodMk_sup'_sup'
deleted theorem Finset.sup'_biUnion
deleted theorem Finset.sup'_inf_sup'
deleted theorem Finset.sup'_prodMap
deleted theorem Finset.sup'_product_left
deleted theorem Finset.sup'_product_right
deleted theorem Finset.sup_biUnion
deleted theorem Finset.sup_eq_biUnion
deleted theorem Finset.sup_inf
deleted theorem Finset.sup_inf_sup
deleted theorem Finset.sup_prodMap
deleted theorem Finset.sup_product_left
deleted theorem Finset.sup_product_right