Commit 2023-03-31 11:27 5cf01000

View on Github →

chore: forward-port mathlib #18682 (#3200)

Estimated changes

Modified Mathlib/Data/Finset/Image.lean

added theorem Finset.image_sdiff

added theorem Finset.image_symmDiff

Modified Mathlib/Data/Finset/Pointwise.lean

added theorem Finset.smul_finset_inter

added theorem Finset.smul_finset_inter₀

added theorem Finset.smul_finset_sdiff

added theorem Finset.smul_finset_sdiff₀

added theorem Finset.smul_finset_symmDiff

added theorem Finset.smul_finset_symm_diff₀

added theorem Finset.smul_finset_univ

added theorem Finset.smul_univ

Modified Mathlib/Data/Set/Pointwise/SMul.lean