primeFactors_mul_eq_union — Mathlib

English

If a and b are nonzero, the prime factors of a b are the union of the prime factors of a and b.

Русский

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

LaTeX

$$$ a \neq 0 \land b \neq 0 \Rightarrow \operatorname{primeFactors}(a b) = \operatorname{primeFactors}(a) \cup \operatorname{primeFactors}(b) $$$

Lean4

theorem primeFactors_mul_eq_union [DecidableEq M] (ha : a ≠ 0) (hb : b ≠ 0) :
    primeFactors (a * b) = primeFactors a ∪ primeFactors b :=
  by
  ext p
  simp [mem_normalizedFactors_iff', mem_primeFactors, ha, hb]

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