Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-17 19:18 ce8a6ca0

View on Github →

refactor(data/multiset/basic): consistently use 'nsmul' in names (#6735)

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem multiset.to_finset_sum_count_nsmul_eq

deleted theorem multiset.to_finset_sum_count_smul_eq

Modified src/data/finsupp/basic.lean

Modified src/data/multiset/basic.lean

added theorem multiset.card_nsmul

deleted theorem multiset.card_smul

added theorem multiset.count_nsmul

deleted theorem multiset.count_smul

added theorem multiset.prod_nsmul

deleted theorem multiset.prod_smul

Modified src/data/multiset/fold.lean

Modified src/data/pnat/factors.lean