multiset ext nodup

Stream: Is there code for X?

[Yaël Dillies]

Do we have such a lemma somewhere?

example {S : multiset ℕ} {s : finset ℕ} (hs : S.nodup) :
  S = s.val ↔ ∀ x, x ∈ S ↔ x ∈ s :=```

[Yakov Pechersky]

Exactly what your topic title is:

variable {α : Type*}
example (S : multiset α) (s : finset α) (hs : S.nodup) :
  S = s.val ↔ ∀ x, x ∈ S ↔ x ∈ s :=
multiset.nodup_ext hs s.nodup

[Yaël Dillies]

Ahahah! I still missed it. Thanks!