Commit 2023-11-13 12:15 1ec654bb

feat: add four lemmas on topological sums (#8325) This adds four API lemmas that are useful for establishing Euler products:

@[simp] lemma hasSum_unique [Unique β] (f : β → α) : HasSum f (f default)
@[simp] lemma hasSum_singleton (m : β) (f : β → α) : HasSum (({m} : Set β).restrict f) (f m)
lemma tsum_setElem_eq_tsum_setElem_diff [T2Space α] {f : β → α} (s t : Set β) (hf₀ : ∀ b ∈ t, f b = 0) :
    ∑' a : s, f a = ∑' a : (s \ t : Set β), f a
lemma tsum_eq_tsum_diff_singleton {α  β : Type*} [AddCommMonoid α] [TopologicalSpace α] [T2Space α]
    {f : β → α} (s : Set β) (b : β) (hf₀ : f b = 0) :
    ∑' a : s, f a = ∑' a : (s \ {b} : Set β), f a