emultiplicity — Mathlib

English

emultiplicity(a,b) is the largest n in ℕ∞ such that a^n divides b, or ∞ if this holds for all n.

Русский

emultiplicity(a,b) наименьшая максимальная степень n, при которой a^n делит b, или ∞, если такова степень бесконечна.

LaTeX

$$$ \operatorname{emultiplicity}(a,b) = \begin{cases} n, & \text{if FiniteMultiplicity}(a,b) \\ \top, & \text{otherwise} \end{cases}$$$

Lean4

/-- `emultiplicity a b` returns the largest natural number `n` such that
  `a ^ n ∣ b`, as an `ℕ∞`. If `∀ n, a ^ n ∣ b` then it returns `⊤`. -/
noncomputable def emultiplicity [Monoid α] (a b : α) : ℕ∞ :=
  if h : FiniteMultiplicity a b then Nat.find h else ⊤

Похожие утверждения