n : ℕ
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
⊢ ∀ (x : ℕ), x ∈ toFinset (factors n) → (fun p x => f p) x (↑(factorization n) x) = f x
n : ℕ
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
⊢ (Finsupp.prod (factorization n) fun p x => f p) = ∏ p in toFinset (factors n), f p
apply prod_congr support_factorization
no goals
n : ℕ
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
⊢ ∀ (x : ℕ), x ∈ toFinset (factors n) → (fun p x => f p) x (↑(factorization n) x) = f x
simp