Commit 2023-04-28 14:14 c813ed7d

View on Github →

chore(data/finset/lattice): Remove finset.sup_finset_image (#18893) in favor of the identical finset.sup_image (up to argument order) in the same file.

Estimated changes

Modified src/data/finset/lattice.lean

deleted theorem finset.sup_finset_image

Modified src/order/compactly_generated.lean

Modified src/ring_theory/finiteness.lean

Modified src/ring_theory/mv_polynomial/symmetric.lean