Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-26 14:24 6ae9f000

View on Github →

feat(ring_theory/polynomial/symmetric): degrees_esymm (#6718) A lot of API also added for finset, finsupp, multiset, powerset_len

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem finset.sum_multiset_singleton

Modified src/data/finset/lattice.lean

modified theorem finset.sup_finset_image

Modified src/data/finset/powerset.lean

added theorem finset.powerset_len_nonempty

added theorem finset.powerset_len_self

added theorem finset.powerset_len_succ_insert

added theorem finset.powerset_len_sup

Modified src/data/finsupp/basic.lean

added theorem finsupp.single_eq_pi_single

added theorem finsupp.support_single_disjoint

added theorem finsupp.support_single_ne_bot

added theorem finsupp.support_sum_eq_bUnion

added theorem finsupp.to_multiset_sum

added theorem finsupp.to_multiset_sum_single

Modified src/data/fintype/basic.lean

added theorem multiset.count_univ

Modified src/data/multiset/lattice.lean

added theorem multiset.nodup_sup_iff

Modified src/data/set/basic.lean

added theorem set.pairwise_on_empty

added theorem set.pairwise_on_insert_of_symmetric

Modified src/data/support.lean

added theorem pi.support_single_disjoint

Modified src/order/compactly_generated.lean

Modified src/ring_theory/noetherian.lean

Modified src/ring_theory/polynomial/symmetric.lean

added theorem mv_polynomial.degrees_esymm

added theorem mv_polynomial.support_esymm''

added theorem mv_polynomial.support_esymm'

added theorem mv_polynomial.support_esymm