matt rice (Jan 03 2021 at 23:21):
Is it weird that
multiset.erase_dup https://github.com/leanprover-community/mathlib/blob/master/src/data/multiset/erase_dup.lean#L19-L20 docs says "yielding a
nodup multiset." but the return value is plain
multiset, e.g. doesn't seem to have any
multiset.nodup, if so would that be a doc issue, definition issue, or me missing something perhaps?
Floris van Doorn (Jan 03 2021 at 23:23):
matt rice (Jan 03 2021 at 23:33):
aha :dizzy:, thanks.
Last updated: May 08 2021 at 04:14 UTC