α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝ : CommMonoid β
a b : ℕ
hab : a < b
f : ℕ → β
ha : ¬a ∈ Ico (a + 1) b
⊢ ∏ k in Ico a b, f k = f a * ∏ k in Ico (a + 1) b, f k
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝ : CommMonoid β
a b : ℕ
hab : a < b
f : ℕ → β
⊢ ∏ k in Ico a b, f k = f a * ∏ k in Ico (a + 1) b, f k
have ha : a ∉ Ico (a + 1) b := by simp
no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝ : CommMonoid β
a b : ℕ
hab : a < b
f : ℕ → β
ha : ¬a ∈ Ico (a + 1) b
⊢ ∏ k in Ico a b, f k = f a * ∏ k in Ico (a + 1) b, f k
rw [← prod_insert ha, Nat.Ico_insert_succ_left hab]
no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝ : CommMonoid β
a b : ℕ
hab : a < b
f : ℕ → β
⊢ ¬a ∈ Ico (a + 1) b
simp