mem_smoothNumbers' — Mathlib

English

m ∈ n.smoothNumbers iff m ≠ 0 and m.primeFactors ⊆ n.primesBelow.

Русский

m ∈ n.smoothNumbers тогда и только тогда, когда m ≠ 0 и m.primeFactors ⊆ n.primesBelow.

LaTeX

$$$m \in n.smoothNumbers \iff m \neq 0 \wedge m.\text{primeFactors} \subseteq n.\text{primesBelow}$$$

Lean4

/-- `m` is `n`-smooth if and only if all prime divisors of `m` are less than `n`. -/
theorem mem_smoothNumbers' {n m : ℕ} : m ∈ smoothNumbers n ↔ ∀ p, p.Prime → p ∣ m → p < n := by
  simp only [smoothNumbers_eq_factoredNumbers, mem_factoredNumbers', Finset.mem_range]

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