English
The cardinality of a multiset equals the sum of the multiplicities of its elements, and is the length of any representing list.
Русский
Кардинал мультисетa равен сумме кратностей его элементов и равен длине любого представления этого мультисетa списком.
LaTeX
$$$\\forall s\\in\\mathcal{M}(\\alpha),\\operatorname{card}(s)=\\sum_{a\\in \\alpha}\\operatorname{mult}(a,s)\\quad\\text{and}\\quad \\operatorname{card}(\\operatorname{ofList}l)=\\operatorname{length}(l).$$$
Lean4
/-- The cardinality of a multiset is the sum of the multiplicities
of all its elements, or simply the length of the underlying list. -/
def card : Multiset α → ℕ :=
Quot.lift length fun _l₁ _l₂ => Perm.length_eq
