mem_factoredNumbers_of_primeFactors_subset

English

If m ≠ 0 and m.primeFactors ⊆ s, then m ∈ factoredNumbers(s).

Русский

Если m ≠ 0 и m.primeFactors ⊆ s, то m ∈ factoredNumbers(s).

LaTeX

$$m ≠ 0 ∧ m.primeFactors ⊆ s ⇒ m ∈ \mathrm{factoredNumbers}(s)$$

Lean4

/-- If `m ≠ 0` and the `Finset` of prime factors of `m` is contained in `s`, then `m`
is `s`-factored. -/
theorem mem_factoredNumbers_of_primeFactors_subset {s : Finset ℕ} {m : ℕ} (hm : m ≠ 0) (hp : m.primeFactors ⊆ s) :
    m ∈ factoredNumbers s := by
  rw [mem_factoredNumbers]
  exact ⟨hm, fun p hp' ↦ hp <| mem_primeFactors_iff_mem_primeFactorsList.mpr hp'⟩

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