nodup vs. count vs length

Stream: Is there code for X?

[Jakob Scholbach]

Is there a statement such as: for a multiset with nodup, the count equals the length?

[Ruben Van de Velde]

I don't see anything at https://leanprover-community.github.io/mathlib_docs/data/multiset/nodup.html , though I don't know what you mean by the count

[Jakob Scholbach]

I meant https://leanprover-community.github.io/mathlib_docs/data/multiset/basic.html#multiset.count

[Yakov Pechersky]

Do you mean that the sum of count should be the length? Should be a simple statement using induction on the multiset ad the existing lemmas, or by lifting the statement about lists that says that lists that are related by a perm must have the same length.

[Mario Carneiro]

I think this theorem exists

[Mario Carneiro]

If you interpret count as erase_dup.length then this is docs#multiset.erase_dup_eq_self

[Mario Carneiro]

The theorem Yakov is talking about is docs#multiset.to_finset_sum_count_eq