Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-22 23:55 416edbd3

View on Github →

chore(ring_theory/polynomial/symmetric): golf proofs (#14866)

Estimated changes

Modified src/data/finset/basic.lean

added theorem equiv.finset_congr_to_embedding

Modified src/data/finset/powerset.lean

added theorem finset.powerset_len_map

Modified src/data/fintype/basic.lean

added theorem finset.map_univ_equiv

added theorem finset.map_univ_of_surjective

Modified src/ring_theory/polynomial/symmetric.lean