Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-25 04:10 9d748f0b

View on Github →

feat(data/finset/basic): mem_map_equiv (#6399) This adds a version of mem_map specialized to equivs, which has a better simp-nf.

Estimated changes

Modified src/data/finset/basic.lean

added theorem equiv.finset_congr_refl

added theorem equiv.finset_congr_symm

deleted theorem equiv.finset_congr_symm_apply

added theorem equiv.finset_congr_trans

added theorem finset.mem_map_equiv

Modified src/ring_theory/polynomial/symmetric.lean