English
Let f be a Nat→R; then IsMultiplicative(prodPrimeFactors f).
Русский
Пусть f:Nat→R; тогда IsMultiplicative(prodPrimeFactors f).
LaTeX
$$$\operatorname{IsMultiplicative}(\operatorname{prodPrimeFactors} f)$$$
Lean4
@[arith_mult]
theorem prodPrimeFactors [CommMonoidWithZero R] (f : ℕ → R) : IsMultiplicative (prodPrimeFactors f) :=
by
rw [iff_ne_zero]
simp only [ne_eq, one_ne_zero, not_false_eq_true, prodPrimeFactors_apply, primeFactors_one, prod_empty, true_and]
intro x y hx hy hxy
have hxy₀ : x * y ≠ 0 := mul_ne_zero hx hy
rw [prodPrimeFactors_apply hxy₀, prodPrimeFactors_apply hx, prodPrimeFactors_apply hy, Nat.primeFactors_mul hx hy, ←
Finset.prod_union hxy.disjoint_primeFactors]