Elements of a multiset without duplicates

Mathlib coerces a multiset m to the type of its elements, where an element is a value of m together with an occurrence index below its multiplicity. When m has no duplicates every value occurs once, so an element is determined by its value: this file records that the coercion to the ambient type is injective.

theorem Multiset.Nodup.coe_injective {α : Type u_1} [DecidableEq α] {m : Multiset α} (h : m.Nodup) : Function.Injective fun (x : m.ToType) => x.fst

For a multiset without duplicates, an element is determined by its value.