Commit 2025-03-18 15:42 a6e8dcef

View on Github →

chore(Data/Finset): remove deprecated lemma Finset.filter_mem_image_eq_image (#23054) This has been deprecated for over 6 months and was blocking a (minor) import reduction.

Estimated changes

Modified Mathlib/Data/Finset/BooleanAlgebra.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Finset/Fold.lean

Modified Mathlib/Data/Finset/Image.lean

deleted theorem Finset.filter_mem_image_eq_image