instDecidablePredMemSetFactoredNumbers

Mathlib.NumberTheory.SmoothNumbers

URI: https://scilib.ai/kg/mathlib#Nat.instDecidablePredMemSetFactoredNumbers

← MathLib Explorer

English

Membership in factoredNumbers(s) is decidable.

Русский

Членство в factoredNumbers(s) разрешимо (решаемо).

LaTeX

$$DecidablePred (\lambda x, x ∈ \mathrm{factoredNumbers}(s))$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru