Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-08 08:00 572e54ab

View on Github →

fix(algebra/big_operators/multiset): rename prod_le_sum_prod to prod_le_prod_map (#16420)

Estimated changes

Modified src/algebra/big_operators/multiset.lean

added theorem multiset.prod_le_prod_map

deleted theorem multiset.prod_le_sum_prod

Modified src/topology/algebra/polynomial.lean