no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝¹ : CommMonoid β
δ : Type u_1
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k in Ico m n, f k) * ∏ k in range m, f k = ∏ k in range n, f k
(rw [mul_comm]; exact prod_range_mul_prod_Ico f h)
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝¹ : CommMonoid β
δ : Type u_1
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k in range m, f k) * ∏ k in Ico m n, f k = ∏ k in range n, f k
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝¹ : CommMonoid β
δ : Type u_1
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k in Ico m n, f k) * ∏ k in range m, f k = ∏ k in range n, f k
rw [mul_comm]
no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝¹ : CommMonoid β
δ : Type u_1
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k in range m, f k) * ∏ k in Ico m n, f k = ∏ k in range n, f k
exact prod_range_mul_prod_Ico f h