mem_factoredNumbers_iff_primeFactors_subset

English

m ∈ factoredNumbers s implies m.primeFactors ⊆ s, and conversely

Русский

Членство m ∈ factoredNumbers s эквивалентно ⊆ свойству m.primeFactors

LaTeX

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

Lean4

/-- `m` is `s`-factored if and only if `m ≠ 0` and its `Finset` of prime factors
is contained in `s`. -/
theorem mem_factoredNumbers_iff_primeFactors_subset {s : Finset ℕ} {m : ℕ} :
    m ∈ factoredNumbers s ↔ m ≠ 0 ∧ m.primeFactors ⊆ s :=
  ⟨fun h ↦ ⟨ne_zero_of_mem_factoredNumbers h, primeFactors_subset_of_mem_factoredNumbers h⟩, fun ⟨h₁, h₂⟩ ↦
    mem_factoredNumbers_of_primeFactors_subset h₁ h₂⟩

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