mem_smoothNumbers — Mathlib

English

For natural numbers n and m, m belongs to smoothNumbers(n) exactly when m ≠ 0 and all prime factors of m are less than n.

Русский

Для натуральных чис n и m выполнение: m ∈ smoothNumbers(n) тогда и только тогда, когда m ≠ 0 и все простые делители m меньше n.

LaTeX

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

Lean4

theorem mem_smoothNumbers {n m : ℕ} : m ∈ smoothNumbers n ↔ m ≠ 0 ∧ ∀ p ∈ primeFactorsList m, p < n :=
  Iff.rfl

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