prodPrimeFactors — Mathlib

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]

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