no goals
ι : Type ?u.620604
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : CommGroup M
f : ℕ → M
n : ℕ
⊢ f n = f 0 * ∏ i in range n, f (i + 1) / f i
rw [prod_range_div, mul_div_cancel'_right]