multiset.erased_dup

Stream: general

[matt rice]

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]

docs#multiset.nodup_erase_dup?

[matt rice]

aha :dizzy:, thanks.