English
The size function sizeOf assigns a natural number to a multiset by referring to the size of a representing list.
Русский
Функция размера sizeOf назначает естественное число мультисету через размер представленного списка.
LaTeX
$$$\\operatorname{sizeOf}(s)=\\text{SizeOf}(s)$ как на представлении через список; размер определяется через представление.$$
Lean4
/-- Defines a size for a multiset by referring to the size of the underlying list.
This has to be defined before the definition of `Finset`, otherwise its automatically generated
`SizeOf` instance will be wrong.
-/
protected def sizeOf [SizeOf α] (s : Multiset α) : ℕ :=
(Quot.liftOn s SizeOf.sizeOf) fun _ _ => Perm.sizeOf_eq_sizeOf
