primeFactors_mul — Mathlib

English

If a and b are coprime, then (ab).primeFactors = a.primeFactors ∪ b.primeFactors.

Русский

Если a и b взаимно просты, то простые делители произведения равны объединению простых делителей a и b.

LaTeX

$$$ \\mathrm{Coprime}(a,b) \\Rightarrow (a b).primeFactors = a.primeFactors \\cup b.primeFactors $$$

Lean4

theorem primeFactors_mul {a b : ℕ} (hab : Coprime a b) : (a * b).primeFactors = a.primeFactors ∪ b.primeFactors :=
  (List.toFinset.ext <| mem_primeFactorsList_mul_of_coprime hab).trans <| List.toFinset_union _ _

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