ι : Type ?u.621749
β : 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 0 * ∏ i in range n, f (i + 1) / f i = ∏ i in range (n + 1), if i = 0 then f 0 else f i / f (i - 1)
ι : Type ?u.621749
β : 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 = ∏ i in range (n + 1), if i = 0 then f 0 else f i / f (i - 1)
conv_lhs => rw [Finset.eq_prod_range_div f]
no goals
ι : Type ?u.621749
β : 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 0 * ∏ i in range n, f (i + 1) / f i = ∏ i in range (n + 1), if i = 0 then f 0 else f i / f (i - 1)
simp [Finset.prod_range_succ', mul_comm]