Commit 2026-04-13 06:55 397bcca0

View on Github →

chore(Data/Finset/Lattice/Prod): use to_dual (#37052)

Estimated changes

Modified Mathlib/Data/Finset/Lattice/Prod.lean

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_prodMap

deleted theorem Finset.inf_product_left

deleted theorem Finset.inf_product_right

deleted theorem Finset.inf_sup_inf

deleted theorem Finset.prodMk_inf'_inf'

modified theorem Finset.sup_prodMap