decidableFiniteMultiplicity — Mathlib

English

There is a decision procedure for FiniteMultiplicity on natural numbers.

Русский

Существует алгоритм решения вопроса о конечности кратности в натуральных числах.

LaTeX

$$$ \text{DecidableRel } (\lambda a b: FiniteMultiplicity a b) $$$

Lean4

instance decidableFiniteMultiplicity : DecidableRel fun a b : ℕ => FiniteMultiplicity a b := fun _ _ ↦
  decidable_of_iff' _ Nat.finiteMultiplicity_iff

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