English
Same as factorization_prod: the factorization of a finite product equals the sum of the factorization of the factors, when all factors are nonzero.
Русский
То же самое, что факторизация произведения: факторизация произведения равна сумме факторизаций составляющих, при условии их не нуля.
LaTeX
$$$ (S.\\mathrm{prod} g).factorization = S.\\mathrm{sum} (\\lambda x. (g x).factorization) \\quad (\\forall x \\in S, g(x) \\neq 0)$$$
Lean4
/-- Any Finsupp `f : ℕ →₀ ℕ` whose support is in the primes is equal to the factorization of
the product `∏ (a : ℕ) ∈ f.support, a ^ f a`. -/
theorem prod_pow_factorization_eq_self {f : ℕ →₀ ℕ} (hf : ∀ p : ℕ, p ∈ f.support → Prime p) :
(f.prod (· ^ ·)).factorization = f :=
by
have h : ∀ x : ℕ, x ∈ f.support → x ^ f x ≠ 0 := fun p hp => pow_ne_zero _ (Prime.ne_zero (hf p hp))
simp only [Finsupp.prod, factorization_prod h]
conv =>
rhs
rw [(sum_single f).symm]
exact sum_congr rfl fun p hp => Prime.factorization_pow (hf p hp)
