English
Define multiplicity(a,b) as the natural-valued version of emultiplicity, namely multiplicity(a,b) = (emultiplicity(a,b)).untopD 1, i.e., take the finite value when it exists and return 1 if emultiplicity is top.
Русский
Определим кратность(a,b) как натуральную версию emultiplicity: multiplicity(a,b) = (emultiplicity(a,b)).untopD 1; то есть на месте ∞ ставится 1.
LaTeX
$$$ \operatorname{multiplicity}(a,b) = \operatorname{untopD}_{1}(\operatorname{emultiplicity}(a,b)) $$$
Lean4
/-- A `ℕ`-valued version of `emultiplicity`, returning `1` instead of `⊤`. -/
noncomputable def multiplicity [Monoid α] (a b : α) : ℕ :=
(emultiplicity a b).untopD 1
