instDecidablePredMemSetSmoothNumbers

English

Membership in the set smoothNumbers(n) is a decidable property.

Русский

Членство в множестве smoothNumbers(n) является распознаваемым свойством.

LaTeX

$$$\text{Decidable}(x \in \mathrm{smoothNumbers}(n))$$$

Lean4

/-- Membership in `Nat.smoothNumbers n` is decidable. -/
instance (n : ℕ) : DecidablePred (· ∈ smoothNumbers n) :=
  inferInstanceAs <| DecidablePred fun x ↦ x ∈ {m | m ≠ 0 ∧ ∀ p ∈ primeFactorsList m, p < n}

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