mul_mem_factoredNumbers — Mathlib

English

The product of two s-factored numbers is s-factored.

Русский

Произведение двух s-факторизованных чисел снова s-факторизовано.

LaTeX

$$m ∈ \mathrm{factoredNumbers}(s) ∧ n ∈ \mathrm{factoredNumbers}(s) ⇒ m n ∈ \mathrm{factoredNumbers}(s)$$

Lean4

/-- The product of two `s`-factored numbers is again `s`-factored. -/
theorem mul_mem_factoredNumbers {s : Finset ℕ} {m n : ℕ} (hm : m ∈ factoredNumbers s) (hn : n ∈ factoredNumbers s) :
    m * n ∈ factoredNumbers s :=
  by
  have hm' := primeFactors_subset_of_mem_factoredNumbers hm
  have hn' := primeFactors_subset_of_mem_factoredNumbers hn
  exact
    mem_factoredNumbers_of_primeFactors_subset (mul_ne_zero hm.1 hn.1) <|
      primeFactors_mul hm.1 hn.1 ▸ Finset.union_subset hm' hn'

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