English
Let p be a prime and s a finite set with f: s → α. Then emultiplicity p (∏ x∈s, f x) equals the sum over s of emultiplicity p (f x).
Русский
Пусть p — простое, и пусть s — конечный множество с отображением f: s → α. Тогда emultiplicity p произведения по s равна сумме emultiplicity p (f x) по всем x∈s.
LaTeX
$$$ emultiplicity p (\prod_{x \in s} f x) = \sum_{x \in s} emultiplicity p (f x) $$$
Lean4
theorem emultiplicity_prod {β : Type*} {p : α} (hp : Prime p) (s : Finset β) (f : β → α) :
emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x) := by
classical
induction s using Finset.induction with
| empty =>
simp only [Finset.sum_empty, Finset.prod_empty]
exact emultiplicity_of_one_right hp.not_unit
| insert a s has ih => simpa [has, ← ih] using emultiplicity_mul hp
