Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-05 20:21 ddfba423

View on Github →

chore(data/multiset/basic): make card a bundled add_monoid_hom (#5228) Other changes:

  • use /-! ### in section headers;
  • move add_monoid section above card;
  • fix docstrings of multiset.choose_x and multiset.choose.

Estimated changes

modified def multiset.card
modified theorem multiset.card_add
modified theorem multiset.count_eq_zero