primeFactors_mul — Mathlib

English

If a ≠ 0 and b ≠ 0, then (a b).primeFactors = a.primeFactors ∪ b.primeFactors.

Русский

Если a ≠ 0 и b ≠ 0, тогда (a b).primeFactors = a.primeFactors ∪ b.primeFactors.

LaTeX

$$$ (a \\neq 0) \\land (b \\neq 0) \\Rightarrow (a b).primeFactors = a.primeFactors \\cup b.primeFactors $$$

Lean4

theorem primeFactors_mul (ha : a ≠ 0) (hb : b ≠ 0) : (a * b).primeFactors = a.primeFactors ∪ b.primeFactors := by ext;
  simp only [Finset.mem_union, mem_primeFactors_iff_mem_primeFactorsList, mem_primeFactorsList_mul ha hb]

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