mem_smoothNumbers_iff_primeFactors_subset

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 an `n`-smooth number if and only if `m ≠ 0` and the `Finset` of its prime factors
is contained in the `Finset` of primes below `n` -/
theorem mem_smoothNumbers_iff_primeFactors_subset {m n : ℕ} :
    m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ m.primeFactors ⊆ n.primesBelow :=
  ⟨fun h ↦ ⟨h.1, primeFactors_subset_of_mem_smoothNumbers h⟩, fun h ↦
    mem_smoothNumbers_of_primeFactors_subset h.1 <| h.2.trans <| Finset.filter_subset ..⟩

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