factoredNumbers — Mathlib

English

For a finite set s of naturals, factoredNumbers(s) is the set of nonzero naturals all of whose prime factors lie in s.

Русский

Для конечного множества s натуральных чисел factoredNumbers(s) есть множество ненулевых чисел, все простые делители которых лежат в s.

LaTeX

$$m ∈ \mathrm{factoredNumbers}(s) \iff m \neq 0 \wedge \forall p \in \mathrm{primeFactorsList}(m), p \in s$$

Lean4

/-- `factoredNumbers s`, for a finite set `s` of natural numbers, is the set of positive natural
numbers all of whose prime factors are in `s`. -/
def factoredNumbers (s : Finset ℕ) : Set ℕ :=
  {m | m ≠ 0 ∧ ∀ p ∈ primeFactorsList m, p ∈ s}

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