From 975031d53f2bc795fc4f71b196693c44345769bb Mon Sep 17 00:00:00 2001
From: Stuart Presnell <stuart.presnell@gmail.com>
Date: Wed, 12 Jan 2022 16:25:20 +0000
Subject: [PATCH] feat(data/nat/factorization): add lemma `factorization_prod`
 (#11395)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

For any `p : ℕ` and any function `g : α → ℕ` that's non-zero on `S : finset α`, the power of `p` in `S.prod g` equals the sum over `x ∈ S` of the powers of `p` in `g x`.

Generalises `factorization_mul`, which is the special case where `S.card = 2` and `g = id`.
---
 src/data/nat/factorization.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/data/nat/factorization.lean b/src/data/nat/factorization.lean
index 1e72eff2df792..e207f3d95babd 100644
--- a/src/data/nat/factorization.lean
+++ b/src/data/nat/factorization.lean
@@ -93,6 +93,20 @@ end
   factorization (p^k) = single p k :=
 by simp [factorization_pow, hp.factorization]
 
+/-- For any `p : ℕ` and any function `g : α → ℕ` that's non-zero on `S : finset α`,
+the power of `p` in `S.prod g` equals the sum over `x ∈ S` of the powers of `p` in `g x`.
+Generalises `factorization_mul`, which is the special case where `S.card = 2` and `g = id`. -/
+lemma factorization_prod {α : Type*} {S : finset α} {g : α → ℕ} (hS : ∀ x ∈ S, g x ≠ 0) :
+  (S.prod g).factorization = S.sum (λ x, (g x).factorization) :=
+begin
+  classical,
+  ext p,
+  apply finset.induction_on' S, { simp },
+  { intros x T hxS hTS hxT IH,
+    have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr (λ x hx, hS x (hTS hx)),
+    simp [prod_insert hxT, sum_insert hxT, ←IH, factorization_mul (hS x hxS) hT] }
+end
+
 /-! ### Factorizations of pairs of coprime numbers -/
 
 /-- The prime factorizations of coprime `a` and `b` are disjoint -/