factorization_prod_apply — Mathlib

English

Let S be a finite set and g: S → ℕ with g(x) ≠ 0 for all x ∈ S. Then (S.prod g).factorization p equals S.sum (g x).factorization p.

Русский

Пусть S — конечное множество, g:S→ℕ, при этом ∀ x∈S, g(x) ≠ 0. Тогда (S.prod g).factorization p = ∑ x∈S (g x).factorization p.

LaTeX

$$$ (S.prod g).factorization p = S.sum (\lambda x => (g x).factorization p) $$$

Lean4

/-- Modified version of `factorization_prod` that accounts for inputs. -/
theorem factorization_prod_apply {α : Type*} {p : ℕ} {S : Finset α} {g : α → ℕ} (hS : ∀ x ∈ S, g x ≠ 0) :
    (S.prod g).factorization p = S.sum fun x => (g x).factorization p := by rw [factorization_prod hS, finset_sum_apply]

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