mathlib3
ddfba423 - chore(data/multiset/basic): make `card` a bundled `add_monoid_hom` (#5228)

Commit
5 years ago
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`.
Author
Parents
Loading