Commit 2023-04-30 17:11 9d684a89

View on Github →

chore(data/finset/lattice): Move lemmas around (#18900) Move map_finset_sup/map_finset_inf from order.hom.lattice to data.finset.lattice. This breaks a few unqualified downstream uses of submodule.map_bot.

Estimated changes

Modified src/data/finset/lattice.lean

modified theorem finset.inf_sdiff_left

modified theorem finset.inf_sdiff_right

modified theorem finset.sup_sdiff_left

added theorem map_finset_inf

added theorem map_finset_sup

Modified src/linear_algebra/basic.lean

Modified src/linear_algebra/finsupp.lean

Modified src/linear_algebra/linear_independent.lean

Modified src/order/hom/complete_lattice.lean

Modified src/order/hom/lattice.lean

deleted theorem map_finset_inf

deleted theorem map_finset_sup