smoothNumbers — Mathlib

English

The set smoothNumbers(n) consists of all positive natural numbers whose prime factors are all less than n.

Русский

Множество smoothNumbers(n) состоит из всех положительных натуральных чисел, все простые делители которых меньше n.

LaTeX

$$$\mathrm{smoothNumbers}(n) = \{ m \in \mathbb{N} : m \neq 0 \wedge \forall p \in \text{primeFactorsList}(m), p < n \}$$$

Lean4

/-- `smoothNumbers n` is the set of *`n`-smooth positive natural numbers*, i.e., the
positive natural numbers all of whose prime factors are less than `n`. -/
def smoothNumbers (n : ℕ) : Set ℕ :=
  {m | m ≠ 0 ∧ ∀ p ∈ primeFactorsList m, p < n}

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