decidableMultiplicityFinite — Mathlib

English

There exists a decision procedure for the relation FiniteMultiplicity on the integers; equivalently, for all a,b ∈ ℤ, FiniteMultiplicity(a,b) is decidable.

Русский

Существует алгоритм определения предиката FiniteMultiplicity(a,b) для любых a,b ∈ ℤ; то есть предикат конечной кратности разрешим.

LaTeX

$$$\\forall a,b \\in \\mathbb{Z},\\ \\text{FiniteMultiplicity}(a,b)\\ \\text{is decidable}$$$

Lean4

instance decidableMultiplicityFinite : DecidableRel fun a b : ℤ => FiniteMultiplicity a b := fun _ _ ↦
  decidable_of_iff' _ Int.finiteMultiplicity_iff

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