α : Type u_1
β : Type ?u.265508
γ : Type ?u.265511
δ : Type ?u.265514
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
he : HasSum (fun k => f (2 * k)) a
ho : HasSum (fun k => f (2 * k + 1)) b
this : Injective ((fun x x_1 => x * x_1) 2)
⊢ HasSum f (a + b)
α : Type u_1
β : Type ?u.265508
γ : Type ?u.265511
δ : Type ?u.265514
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
he : HasSum (fun k => f (2 * k)) a
ho : HasSum (fun k => f (2 * k + 1)) b
⊢ HasSum f (a + b)
have := mul_right_injective₀ (two_ne_zero' ℕ)
α : Type u_1
β : Type ?u.265508
γ : Type ?u.265511
δ : Type ?u.265514
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
ho : HasSum (fun k => f (2 * k + 1)) b
this : Injective ((fun x x_1 => x * x_1) 2)
he : HasSum (fun x => f ↑x) a
⊢ HasSum f (a + b)
α : Type u_1
β : Type ?u.265508
γ : Type ?u.265511
δ : Type ?u.265514
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
he : HasSum (fun k => f (2 * k)) a
ho : HasSum (fun k => f (2 * k + 1)) b
this : Injective ((fun x x_1 => x * x_1) 2)
⊢ HasSum f (a + b)
replace he := this.hasSum_range_iff.2 he
α : Type u_1
β : Type ?u.265508
γ : Type ?u.265511
δ : Type ?u.265514
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
this : Injective ((fun x x_1 => x * x_1) 2)
he : HasSum (fun x => f ↑x) a
ho : HasSum (fun x => f ↑x) b
⊢ HasSum f (a + b)
α : Type u_1
β : Type ?u.265508
γ : Type ?u.265511
δ : Type ?u.265514
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
ho : HasSum (fun k => f (2 * k + 1)) b
this : Injective ((fun x x_1 => x * x_1) 2)
he : HasSum (fun x => f ↑x) a
⊢ HasSum f (a + b)
replace ho := ((add_left_injective 1).comp this).hasSum_range_iff.2 ho
α : Type u_1
β : Type ?u.265508
γ : Type ?u.265511
δ : Type ?u.265514
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
this : Injective ((fun x x_1 => x * x_1) 2)
he : HasSum (fun x => f ↑x) a
ho : HasSum (fun x => f ↑x) b
⊢ IsCompl (Set.range ((fun x x_1 => x * x_1) 2)) (Set.range ((fun x => x + 1) ∘ (fun x x_1 => x * x_1) 2))
α : Type u_1
β : Type ?u.265508
γ : Type ?u.265511
δ : Type ?u.265514
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
this : Injective ((fun x x_1 => x * x_1) 2)
he : HasSum (fun x => f ↑x) a
ho : HasSum (fun x => f ↑x) b
⊢ HasSum f (a + b)
refine' he.add_isCompl _ ho