diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index 33a0a0aea8a8b..39b65dfe09ebe 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -502,15 +502,15 @@ noncomputable def normed_space.of_core (α : Type*) (β : Type*)
 
 end normed_space
 
-section has_sum
+section summable
 local attribute [instance] classical.prop_decidable
 open finset filter
 variables [normed_group α] [complete_space α]
 
-lemma has_sum_iff_vanishing_norm {f : ι → α} :
-  has_sum f ↔ ∀ε>0, (∃s:finset ι, ∀t, disjoint t s → ∥ t.sum f ∥ < ε) :=
+lemma summable_iff_vanishing_norm {f : ι → α} :
+  summable f ↔ ∀ε>0, (∃s:finset ι, ∀t, disjoint t s → ∥ t.sum f ∥ < ε) :=
 begin
-  simp only [has_sum_iff_vanishing, metric.mem_nhds_iff, exists_imp_distrib],
+  simp only [summable_iff_vanishing, metric.mem_nhds_iff, exists_imp_distrib],
   split,
   { assume h ε hε, refine h {x | ∥x∥ < ε} ε hε _, rw [ball_0_eq ε] },
   { assume h s ε hε hs,
@@ -520,27 +520,27 @@ begin
     exact ht u hu }
 end
 
-lemma has_sum_of_norm_bounded {f : ι → α} (g : ι → ℝ) (hf : has_sum g) (h : ∀i, ∥f i∥ ≤ g i) :
-  has_sum f :=
-has_sum_iff_vanishing_norm.2 $ assume ε hε,
-  let ⟨s, hs⟩ := has_sum_iff_vanishing_norm.1 hf ε hε in
+lemma summable_of_norm_bounded {f : ι → α} (g : ι → ℝ) (hf : summable g) (h : ∀i, ∥f i∥ ≤ g i) :
+  summable f :=
+summable_iff_vanishing_norm.2 $ assume ε hε,
+  let ⟨s, hs⟩ := summable_iff_vanishing_norm.1 hf ε hε in
   ⟨s, assume t ht,
     have ∥t.sum g∥ < ε := hs t ht,
     have nn : 0 ≤ t.sum g := finset.zero_le_sum (assume a _, le_trans (norm_nonneg _) (h a)),
     lt_of_le_of_lt (norm_triangle_sum t f) $ lt_of_le_of_lt (finset.sum_le_sum $ assume i _, h i) $
       by rwa [real.norm_eq_abs, abs_of_nonneg nn] at this⟩
 
-lemma has_sum_of_has_sum_norm {f : ι → α} (hf : has_sum (λa, ∥f a∥)) : has_sum f :=
-has_sum_of_norm_bounded _ hf (assume i, le_refl _)
+lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
+summable_of_norm_bounded _ hf (assume i, le_refl _)
 
-lemma norm_tsum_le_tsum_norm {f : ι → α} (hf : has_sum (λi, ∥f i∥)) : ∥(∑i, f i)∥ ≤ (∑ i, ∥f i∥) :=
+lemma norm_tsum_le_tsum_norm {f : ι → α} (hf : summable (λi, ∥f i∥)) : ∥(∑i, f i)∥ ≤ (∑ i, ∥f i∥) :=
 have h₁ : tendsto (λs:finset ι, ∥s.sum f∥) at_top (nhds ∥(∑ i, f i)∥) :=
-  (is_sum_tsum $ has_sum_of_has_sum_norm hf).comp (continuous_norm.tendsto _),
+  (has_sum_tsum $ summable_of_summable_norm hf).comp (continuous_norm.tendsto _),
 have h₂ : tendsto (λs:finset ι, s.sum (λi, ∥f i∥)) at_top (nhds (∑ i, ∥f i∥)) :=
-  is_sum_tsum hf,
+  has_sum_tsum hf,
 le_of_tendsto_of_tendsto at_top_ne_bot h₁ h₂ $ univ_mem_sets' $ assume s, norm_triangle_sum _ _
 
-end has_sum
+end summable
 
 namespace complex
 
diff --git a/src/analysis/specific_limits.lean b/src/analysis/specific_limits.lean
index 7cc154757c540..623647533db6c 100644
--- a/src/analysis/specific_limits.lean
+++ b/src/analysis/specific_limits.lean
@@ -15,11 +15,11 @@ open classical function lattice filter finset metric
 
 variables {α : Type*} {β : Type*} {ι : Type*}
 
-lemma has_sum_of_absolute_convergence_real {f : ℕ → ℝ} :
-  (∃r, tendsto (λn, (range n).sum (λi, abs (f i))) at_top (nhds r)) → has_sum f
+lemma summable_of_absolute_convergence_real {f : ℕ → ℝ} :
+  (∃r, tendsto (λn, (range n).sum (λi, abs (f i))) at_top (nhds r)) → summable f
 | ⟨r, hr⟩ :=
   begin
-    refine has_sum_of_has_sum_norm ⟨r, (is_sum_iff_tendsto_nat_of_nonneg _ _).2 _⟩,
+    refine summable_of_summable_norm ⟨r, (has_sum_iff_tendsto_nat_of_nonneg _ _).2 _⟩,
     exact assume i, norm_nonneg _,
     simpa only using hr
   end
@@ -78,20 +78,20 @@ lemma tendsto_one_div_add_at_top_nhds_0_nat :
 suffices tendsto (λ n : ℕ, 1 / (↑(n + 1) : ℝ)) at_top (nhds 0), by simpa,
 (tendsto_add_at_top_iff_nat 1).2 tendsto_one_div_at_top_nhds_0_nat
 
-lemma is_sum_geometric {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
-  is_sum (λn:ℕ, r ^ n) (1 / (1 - r)) :=
+lemma has_sum_geometric {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
+  has_sum (λn:ℕ, r ^ n) (1 / (1 - r)) :=
 have r ≠ 1, from ne_of_lt h₂,
 have r + -1 ≠ 0,
   by rw [←sub_eq_add_neg, ne, sub_eq_iff_eq_add]; simp; assumption,
 have tendsto (λn, (r ^ n - 1) * (r - 1)⁻¹) at_top (nhds ((0 - 1) * (r - 1)⁻¹)),
   from tendsto_mul
     (tendsto_sub (tendsto_pow_at_top_nhds_0_of_lt_1 h₁ h₂) tendsto_const_nhds) tendsto_const_nhds,
-(is_sum_iff_tendsto_nat_of_nonneg (pow_nonneg h₁) _).mpr $
+(has_sum_iff_tendsto_nat_of_nonneg (pow_nonneg h₁) _).mpr $
   by simp [neg_inv, geom_sum, div_eq_mul_inv, *] at *
 
-lemma is_sum_geometric_two (a : ℝ) : is_sum (λn:ℕ, (a / 2) / 2 ^ n) a :=
+lemma has_sum_geometric_two (a : ℝ) : has_sum (λn:ℕ, (a / 2) / 2 ^ n) a :=
 begin
-  convert is_sum_mul_left (a / 2) (is_sum_geometric
+  convert has_sum_mul_left (a / 2) (has_sum_geometric
     (le_of_lt one_half_pos) one_half_lt_one),
   { funext n, simp,
     rw ← pow_inv; [refl, exact two_ne_zero] },
@@ -99,15 +99,15 @@ begin
 end
 
 def pos_sum_of_encodable {ε : ℝ} (hε : 0 < ε)
-  (ι) [encodable ι] : {ε' : ι → ℝ // (∀ i, 0 < ε' i) ∧ ∃ c, is_sum ε' c ∧ c ≤ ε} :=
+  (ι) [encodable ι] : {ε' : ι → ℝ // (∀ i, 0 < ε' i) ∧ ∃ c, has_sum ε' c ∧ c ≤ ε} :=
 begin
   let f := λ n, (ε / 2) / 2 ^ n,
-  have hf : is_sum f ε := is_sum_geometric_two _,
+  have hf : has_sum f ε := has_sum_geometric_two _,
   have f0 : ∀ n, 0 < f n := λ n, div_pos (half_pos hε) (pow_pos two_pos _),
   refine ⟨f ∘ encodable.encode, λ i, f0 _, _⟩,
-  rcases has_sum_comp_of_has_sum_of_injective f (has_sum_spec hf) (@encodable.encode_injective ι _)
+  rcases summable_comp_of_summable_of_injective f (summable_spec hf) (@encodable.encode_injective ι _)
     with ⟨c, hg⟩,
-  refine ⟨c, hg, is_sum_le_inj _ (@encodable.encode_injective ι _) _ _ hg hf⟩,
+  refine ⟨c, hg, has_sum_le_inj _ (@encodable.encode_injective ι _) _ _ hg hf⟩,
   { assume i _, exact le_of_lt (f0 _) },
   { assume n, exact le_refl _ }
 end
@@ -115,9 +115,9 @@ end
 lemma cauchy_seq_of_le_geometric [metric_space α] (r C : ℝ) (hr : r < 1) {f : ℕ → α}
   (hu : ∀n, dist (f n) (f (n+1)) ≤ C * r^n) : cauchy_seq f :=
 begin
-  refine cauchy_seq_of_has_sum_dist (has_sum_of_norm_bounded (λn, C * r^n) _ _),
+  refine cauchy_seq_of_summable_dist (summable_of_norm_bounded (λn, C * r^n) _ _),
   { by_cases h : C = 0,
-    { simp [h, has_sum_zero] },
+    { simp [h, summable_zero] },
     { have Cpos : C > 0,
       { have := le_trans dist_nonneg (hu 0),
         simp only [mul_one, pow_zero] at this,
@@ -126,8 +126,8 @@ begin
       { have := le_trans dist_nonneg (hu 1),
         simp only [pow_one] at this,
         exact nonneg_of_mul_nonneg_left this Cpos },
-      refine has_sum_mul_left C _,
-      exact has_sum_spec (@is_sum_geometric r rnonneg hr) }},
+      refine summable_mul_left C _,
+      exact summable_spec (@has_sum_geometric r rnonneg hr) }},
   show ∀n, abs (dist (f n) (f (n+1))) ≤ C * r^n,
   { assume n, rw abs_of_nonneg (dist_nonneg), exact hu n }
 end
@@ -135,11 +135,11 @@ end
 namespace nnreal
 
 theorem exists_pos_sum_of_encodable {ε : nnreal} (hε : 0 < ε) (ι) [encodable ι] :
-  ∃ ε' : ι → nnreal, (∀ i, 0 < ε' i) ∧ ∃c, is_sum ε' c ∧ c < ε :=
+  ∃ ε' : ι → nnreal, (∀ i, 0 < ε' i) ∧ ∃c, has_sum ε' c ∧ c < ε :=
 let ⟨a, a0, aε⟩ := dense hε in
 let ⟨ε', hε', c, hc, hcε⟩ := pos_sum_of_encodable a0 ι in
 ⟨ λi, ⟨ε' i, le_of_lt $ hε' i⟩, assume i, nnreal.coe_lt.2 $ hε' i,
-  ⟨c, is_sum_le (assume i, le_of_lt $ hε' i) is_sum_zero hc ⟩, nnreal.is_sum_coe.1 hc,
+  ⟨c, has_sum_le (assume i, le_of_lt $ hε' i) has_sum_zero hc ⟩, nnreal.has_sum_coe.1 hc,
    lt_of_le_of_lt (nnreal.coe_le.1 hcε) aε ⟩
 
 end nnreal
diff --git a/src/measure_theory/probability_mass_function.lean b/src/measure_theory/probability_mass_function.lean
index 11e5a5321c220..8f01891efa19a 100644
--- a/src/measure_theory/probability_mass_function.lean
+++ b/src/measure_theory/probability_mass_function.lean
@@ -11,7 +11,7 @@ variables {α : Type*} {β : Type*} {γ : Type*}
 local attribute [instance] classical.prop_decidable
 
 /-- Probability mass functions, i.e. discrete probability measures -/
-def {u} pmf (α : Type u) : Type u := { f : α → nnreal // is_sum f 1 }
+def {u} pmf (α : Type u) : Type u := { f : α → nnreal // has_sum f 1 }
 
 namespace pmf
 
@@ -20,26 +20,26 @@ instance : has_coe_to_fun (pmf α) := ⟨λp, α → nnreal, λp a, p.1 a⟩
 @[extensionality] protected lemma ext : ∀{p q : pmf α}, (∀a, p a = q a) → p = q
 | ⟨f, hf⟩ ⟨g, hg⟩ eq :=  subtype.eq $ funext eq
 
-lemma is_sum_coe_one (p : pmf α) : is_sum p 1 := p.2
+lemma has_sum_coe_one (p : pmf α) : has_sum p 1 := p.2
 
-lemma has_sum_coe (p : pmf α) : has_sum p := has_sum_spec p.is_sum_coe_one
+lemma summable_coe (p : pmf α) : summable p := summable_spec p.has_sum_coe_one
 
-@[simp] lemma tsum_coe (p : pmf α) : (∑a, p a) = 1 := tsum_eq_is_sum p.is_sum_coe_one
+@[simp] lemma tsum_coe (p : pmf α) : (∑a, p a) = 1 := tsum_eq_has_sum p.has_sum_coe_one
 
 def support (p : pmf α) : set α := {a | p.1 a ≠ 0}
 
-def pure (a : α) : pmf α := ⟨λa', if a' = a then 1 else 0, is_sum_ite_eq _ _⟩
+def pure (a : α) : pmf α := ⟨λa', if a' = a then 1 else 0, has_sum_ite_eq _ _⟩
 
 @[simp] lemma pure_apply (a a' : α) : pure a a' = (if a' = a then 1 else 0) := rfl
 
 instance [inhabited α] : inhabited (pmf α) := ⟨pure (default α)⟩
 
 lemma coe_le_one (p : pmf α) (a : α) : p a ≤ 1 :=
-is_sum_le (by intro b; split_ifs; simp [h]; exact le_refl _) (is_sum_ite_eq a (p a)) p.2
+has_sum_le (by intro b; split_ifs; simp [h]; exact le_refl _) (has_sum_ite_eq a (p a)) p.2
 
-protected lemma bind.has_sum (p : pmf α) (f : α → pmf β) (b : β) : has_sum (λa:α, p a * f a b) :=
+protected lemma bind.summable (p : pmf α) (f : α → pmf β) (b : β) : summable (λa:α, p a * f a b) :=
 begin
-  refine nnreal.has_sum_of_le (assume a, _) p.has_sum_coe,
+  refine nnreal.summable_of_le (assume a, _) p.summable_coe,
   suffices : p a * f a b ≤ p a * 1, { simpa },
   exact mul_le_mul_of_nonneg_left ((f a).coe_le_one _) (p a).2
 end
@@ -47,17 +47,17 @@ end
 def bind (p : pmf α) (f : α → pmf β) : pmf β :=
 ⟨λb, (∑a, p a * f a b),
   begin
-    simp [ennreal.is_sum_coe.symm, (ennreal.tsum_coe (bind.has_sum p f _)).symm],
-    rw [is_sum_iff_of_has_sum ennreal.has_sum, ennreal.tsum_comm],
-    simp [ennreal.mul_tsum, (ennreal.tsum_coe (f _).has_sum_coe),
-      ennreal.tsum_coe p.has_sum_coe]
+    simp [ennreal.has_sum_coe.symm, (ennreal.tsum_coe (bind.summable p f _)).symm],
+    rw [has_sum_iff_of_summable ennreal.summable, ennreal.tsum_comm],
+    simp [ennreal.mul_tsum, (ennreal.tsum_coe (f _).summable_coe),
+      ennreal.tsum_coe p.summable_coe]
   end⟩
 
 @[simp] lemma bind_apply (p : pmf α) (f : α → pmf β) (b : β) : p.bind f b = (∑a, p a * f a b) := rfl
 
 lemma coe_bind_apply (p : pmf α) (f : α → pmf β) (b : β) :
   (p.bind f b : ennreal) = (∑a, p a * f a b) :=
-eq.trans (ennreal.tsum_coe $ bind.has_sum p f b).symm $ by simp
+eq.trans (ennreal.tsum_coe $ bind.summable p f b).symm $ by simp
 
 @[simp] lemma pure_bind (a : α) (f : α → pmf β) : (pure a).bind f = f a :=
 have ∀b a', ite (a' = a) 1 0 * f a' b = ite (a' = a) (f a b) 0, from
@@ -109,12 +109,12 @@ def of_multiset (s : multiset α) (hs : s ≠ 0) : pmf α :=
     by rw [← nnreal.eq_iff, nnreal.coe_one, ← this, nnreal.sum_coe]; simp,
   begin
     rw ← this,
-    apply is_sum_sum_of_ne_finset_zero,
+    apply has_sum_sum_of_ne_finset_zero,
     simp {contextual := tt},
   end⟩
 
 def of_fintype [fintype α] (f : α → nnreal) (h : finset.univ.sum f = 1) : pmf α :=
-⟨f, h ▸ is_sum_sum_of_ne_finset_zero (by simp)⟩
+⟨f, h ▸ has_sum_sum_of_ne_finset_zero (by simp)⟩
 
 def bernoulli (p : nnreal) (h : p ≤ 1) : pmf bool :=
 of_fintype (λb, cond b p (1 - p)) (nnreal.eq $ by simp [h])
diff --git a/src/topology/algebra/infinite_sum.lean b/src/topology/algebra/infinite_sum.lean
index 6f0546d795551..0f5a5dfef890e 100644
--- a/src/topology/algebra/infinite_sum.lean
+++ b/src/topology/algebra/infinite_sum.lean
@@ -10,7 +10,7 @@ permutations. For Euclidean spaces (finite dimensional Banach spaces) this is eq
 convergence.
 
 Note: There are summable sequences which are not unconditionally convergent! The other way holds
-generally, see `tendsto_sum_nat_of_is_sum`.
+generally, see `tendsto_sum_nat_of_has_sum`.
 
 Reference:
 * Bourbaki: General Topology (1995), Chapter 3 §5 (Infinite sums in commutative groups)
@@ -30,7 +30,7 @@ def option.cases_on' {α β} : option α → β → (α → β) → β
 
 variables {α : Type*} {β : Type*} {γ : Type*}
 
-section is_sum
+section has_sum
 variables [add_comm_monoid α] [topological_space α] [topological_add_monoid α]
 
 /-- Infinite sum on a topological monoid
@@ -40,60 +40,60 @@ sum operator.
 
 This is based on Mario Carneiro's infinite sum in Metamath.
 -/
-def is_sum (f : β → α) (a : α) : Prop := tendsto (λs:finset β, s.sum f) at_top (nhds a)
+def has_sum (f : β → α) (a : α) : Prop := tendsto (λs:finset β, s.sum f) at_top (nhds a)
 
-/-- `has_sum f` means that `f` has some (infinite) sum. Use `tsum` to get the value. -/
-def has_sum (f : β → α) : Prop := ∃a, is_sum f a
+/-- `summable f` means that `f` has some (infinite) sum. Use `tsum` to get the value. -/
+def summable (f : β → α) : Prop := ∃a, has_sum f a
 
 /-- `tsum f` is the sum of `f` it exists, or 0 otherwise -/
-def tsum (f : β → α) := if h : has_sum f then classical.some h else 0
+def tsum (f : β → α) := if h : summable f then classical.some h else 0
 
 notation `∑` binders `, ` r:(scoped f, tsum f) := r
 
 variables {f g : β → α} {a b : α} {s : finset β}
 
-lemma is_sum_tsum (ha : has_sum f) : is_sum f (∑b, f b) :=
+lemma has_sum_tsum (ha : summable f) : has_sum f (∑b, f b) :=
 by simp [ha, tsum]; exact some_spec ha
 
-lemma has_sum_spec (ha : is_sum f a) : has_sum f := ⟨a, ha⟩
+lemma summable_spec (ha : has_sum f a) : summable f := ⟨a, ha⟩
 
-lemma is_sum_zero : is_sum (λb, 0 : β → α) 0 :=
-by simp [is_sum, tendsto_const_nhds]
+lemma has_sum_zero : has_sum (λb, 0 : β → α) 0 :=
+by simp [has_sum, tendsto_const_nhds]
 
-lemma has_sum_zero : has_sum (λb, 0 : β → α) := has_sum_spec is_sum_zero
+lemma summable_zero : summable (λb, 0 : β → α) := summable_spec has_sum_zero
 
-lemma is_sum_add (hf : is_sum f a) (hg : is_sum g b) : is_sum (λb, f b + g b) (a + b) :=
-by simp [is_sum, sum_add_distrib]; exact tendsto_add hf hg
+lemma has_sum_add (hf : has_sum f a) (hg : has_sum g b) : has_sum (λb, f b + g b) (a + b) :=
+by simp [has_sum, sum_add_distrib]; exact tendsto_add hf hg
 
-lemma has_sum_add (hf : has_sum f) (hg : has_sum g) : has_sum (λb, f b + g b) :=
-has_sum_spec $ is_sum_add (is_sum_tsum hf)(is_sum_tsum hg)
+lemma summable_add (hf : summable f) (hg : summable g) : summable (λb, f b + g b) :=
+summable_spec $ has_sum_add (has_sum_tsum hf)(has_sum_tsum hg)
 
-lemma is_sum_sum {f : γ → β → α} {a : γ → α} {s : finset γ} :
-  (∀i∈s, is_sum (f i) (a i)) → is_sum (λb, s.sum $ λi, f i b) (s.sum a) :=
-finset.induction_on s (by simp [is_sum_zero]) (by simp [is_sum_add] {contextual := tt})
+lemma has_sum_sum {f : γ → β → α} {a : γ → α} {s : finset γ} :
+  (∀i∈s, has_sum (f i) (a i)) → has_sum (λb, s.sum $ λi, f i b) (s.sum a) :=
+finset.induction_on s (by simp [has_sum_zero]) (by simp [has_sum_add] {contextual := tt})
 
-lemma has_sum_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, has_sum (f i)) :
-  has_sum (λb, s.sum $ λi, f i b) :=
-has_sum_spec $ is_sum_sum $ assume i hi, is_sum_tsum $ hf i hi
+lemma summable_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, summable (f i)) :
+  summable (λb, s.sum $ λi, f i b) :=
+summable_spec $ has_sum_sum $ assume i hi, has_sum_tsum $ hf i hi
 
-lemma is_sum_sum_of_ne_finset_zero (hf : ∀b∉s, f b = 0) : is_sum f (s.sum f) :=
+lemma has_sum_sum_of_ne_finset_zero (hf : ∀b∉s, f b = 0) : has_sum f (s.sum f) :=
 tendsto_infi' s $ tendsto.congr'
   (assume t (ht : s ⊆ t), show s.sum f = t.sum f, from sum_subset ht $ assume x _, hf _)
   tendsto_const_nhds
 
-lemma has_sum_sum_of_ne_finset_zero (hf : ∀b∉s, f b = 0) : has_sum f :=
-has_sum_spec $ is_sum_sum_of_ne_finset_zero hf
+lemma summable_sum_of_ne_finset_zero (hf : ∀b∉s, f b = 0) : summable f :=
+summable_spec $ has_sum_sum_of_ne_finset_zero hf
 
-lemma is_sum_ite_eq (b : β) (a : α) : is_sum (λb', if b' = b then a else 0) a :=
+lemma has_sum_ite_eq (b : β) (a : α) : has_sum (λb', if b' = b then a else 0) a :=
 suffices
-  is_sum (λb', if b' = b then a else 0) (({b} : finset β).sum (λb', if b' = b then a else 0)), from
+  has_sum (λb', if b' = b then a else 0) (({b} : finset β).sum (λb', if b' = b then a else 0)), from
   by simpa,
-is_sum_sum_of_ne_finset_zero $ assume b' hb,
+has_sum_sum_of_ne_finset_zero $ assume b' hb,
   have b' ≠ b, by simpa using hb,
   by rw [if_neg this]
 
-lemma is_sum_of_iso {j : γ → β} {i : β → γ}
-  (hf : is_sum f a) (h₁ : ∀x, i (j x) = x) (h₂ : ∀x, j (i x) = x) : is_sum (f ∘ j) a :=
+lemma has_sum_of_iso {j : γ → β} {i : β → γ}
+  (hf : has_sum f a) (h₁ : ∀x, i (j x) = x) (h₂ : ∀x, j (i x) = x) : has_sum (f ∘ j) a :=
 have ∀x y, j x = j y → x = y,
   from assume x y h,
   have i (j x) = i (j y), by rw [h],
@@ -103,24 +103,24 @@ have (λs:finset γ, s.sum (f ∘ j)) = (λs:finset β, s.sum f) ∘ (λs:finset
 show tendsto (λs:finset γ, s.sum (f ∘ j)) at_top (nhds a),
    by rw [this]; apply (tendsto_finset_image_at_top_at_top h₂).comp hf
 
-lemma is_sum_iff_is_sum_of_iso {j : γ → β} (i : β → γ)
+lemma has_sum_iff_has_sum_of_iso {j : γ → β} (i : β → γ)
   (h₁ : ∀x, i (j x) = x) (h₂ : ∀x, j (i x) = x) :
-  is_sum (f ∘ j) a ↔ is_sum f a :=
+  has_sum (f ∘ j) a ↔ has_sum f a :=
 iff.intro
   (assume hfj,
-    have is_sum ((f ∘ j) ∘ i) a, from is_sum_of_iso hfj h₂ h₁,
+    have has_sum ((f ∘ j) ∘ i) a, from has_sum_of_iso hfj h₂ h₁,
     by simp [(∘), h₂] at this; assumption)
-  (assume hf, is_sum_of_iso hf h₁ h₂)
+  (assume hf, has_sum_of_iso hf h₁ h₂)
 
-lemma is_sum_hom (g : α → γ) [add_comm_monoid γ] [topological_space γ] [topological_add_monoid γ]
-  [is_add_monoid_hom g] (h₃ : continuous g) (hf : is_sum f a) :
-  is_sum (g ∘ f) (g a) :=
+lemma has_sum_hom (g : α → γ) [add_comm_monoid γ] [topological_space γ] [topological_add_monoid γ]
+  [is_add_monoid_hom g] (h₃ : continuous g) (hf : has_sum f a) :
+  has_sum (g ∘ f) (g a) :=
 have (λs:finset β, s.sum (g ∘ f)) = g ∘ (λs:finset β, s.sum f),
   from funext $ assume s, sum_hom g,
 show tendsto (λs:finset β, s.sum (g ∘ f)) at_top (nhds (g a)),
   by rw [this]; exact hf.comp (continuous_iff_continuous_at.mp h₃ a)
 
-lemma tendsto_sum_nat_of_is_sum {f : ℕ → α} (h : is_sum f a) :
+lemma tendsto_sum_nat_of_has_sum {f : ℕ → α} (h : has_sum f a) :
   tendsto (λn:ℕ, (range n).sum f) at_top (nhds a) :=
 suffices map (λ (n : ℕ), sum (range n) f) at_top ≤ map (λ (s : finset ℕ), sum s f) at_top,
   from le_trans this h,
@@ -128,8 +128,8 @@ assume s (hs : {t : finset ℕ | t.sum f ∈ s} ∈ at_top),
 let ⟨t, ht⟩ := mem_at_top_sets.mp hs, ⟨n, hn⟩ := @exists_nat_subset_range t in
 mem_at_top_sets.mpr ⟨n, assume n' hn', ht _ $ finset.subset.trans hn $ range_subset.mpr hn'⟩
 
-lemma is_sum_sigma [regular_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} {a : α}
-  (hf : ∀b, is_sum (λc, f ⟨b, c⟩) (g b)) (ha : is_sum f a) : is_sum g a :=
+lemma has_sum_sigma [regular_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} {a : α}
+  (hf : ∀b, has_sum (λc, f ⟨b, c⟩) (g b)) (ha : has_sum f a) : has_sum g a :=
 assume s' hs',
 let
   ⟨s, hs, hss', hsc⟩ := nhds_is_closed hs',
@@ -172,30 +172,30 @@ mem_at_top_sets.mpr $ exists.intro fsts $ assume bs (hbs : fsts ⊆ bs),
         neq_bot_of_le_neq_bot (h _) (le_trans (set.inter_subset_inter (le_trans this hs₂) hs₃) hs₁),
   hss' this
 
-lemma has_sum_sigma [regular_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
-  (hf : ∀b, has_sum (λc, f ⟨b, c⟩)) (ha : has_sum f) : has_sum (λb, ∑c, f ⟨b, c⟩):=
-has_sum_spec $ is_sum_sigma (assume b, is_sum_tsum $ hf b) (is_sum_tsum ha)
+lemma summable_sigma [regular_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
+  (hf : ∀b, summable (λc, f ⟨b, c⟩)) (ha : summable f) : summable (λb, ∑c, f ⟨b, c⟩):=
+summable_spec $ has_sum_sigma (assume b, has_sum_tsum $ hf b) (has_sum_tsum ha)
 
-end is_sum
+end has_sum
 
-section is_sum_iff_is_sum_of_iso_ne_zero
+section has_sum_iff_has_sum_of_iso_ne_zero
 variables [add_comm_monoid α] [topological_space α] [topological_add_monoid α]
 variables {f : β → α} {g : γ → α} {a : α}
 
-lemma is_sum_of_is_sum
+lemma has_sum_of_has_sum
   (h_eq : ∀u:finset γ, ∃v:finset β, ∀v', v ⊆ v' → ∃u', u ⊆ u' ∧ u'.sum g = v'.sum f)
-  (hf : is_sum g a) : is_sum f a :=
+  (hf : has_sum g a) : has_sum f a :=
 suffices at_top.map (λs:finset β, s.sum f) ≤ at_top.map (λs:finset γ, s.sum g),
   from le_trans this hf,
 by rw [map_at_top_eq, map_at_top_eq];
 from (le_infi $ assume b, let ⟨v, hv⟩ := h_eq b in infi_le_of_le v $
   by simp [set.image_subset_iff]; exact hv)
 
-lemma is_sum_iff_is_sum
+lemma has_sum_iff_has_sum
   (h₁ : ∀u:finset γ, ∃v:finset β, ∀v', v ⊆ v' → ∃u', u ⊆ u' ∧ u'.sum g = v'.sum f)
   (h₂ : ∀v:finset β, ∃u:finset γ, ∀u', u ⊆ u' → ∃v', v ⊆ v' ∧ v'.sum f = u'.sum g) :
-  is_sum f a ↔ is_sum g a :=
-⟨is_sum_of_is_sum h₂, is_sum_of_is_sum h₁⟩
+  has_sum f a ↔ has_sum g a :=
+⟨has_sum_of_has_sum h₂, has_sum_of_has_sum h₁⟩
 
 variables
   (i : Π⦃c⦄, g c ≠ 0 → β) (hi : ∀⦃c⦄ (h : g c ≠ 0), f (i h) ≠ 0)
@@ -205,7 +205,7 @@ variables
   (hgj : ∀⦃b⦄ (h : f b ≠ 0), g (j h) = f b)
 include hi hj hji hij hgj
 
-lemma is_sum_of_is_sum_ne_zero : is_sum g a → is_sum f a :=
+lemma has_sum_of_has_sum_ne_zero : has_sum g a → has_sum f a :=
 have j_inj : ∀x y (hx : f x ≠ 0) (hy : f y ≠ 0), (j hx = j hy ↔ x = y),
   from assume x y hx hy,
   ⟨assume h,
@@ -214,7 +214,7 @@ have j_inj : ∀x y (hx : f x ≠ 0) (hy : f y ≠ 0), (j hx = j hy ↔ x = y),
   by simp {contextual := tt}⟩,
 let ii : finset γ → finset β := λu, u.bind $ λc, if h : g c = 0 then ∅ else {i h} in
 let jj : finset β → finset γ := λv, v.bind $ λb, if h : f b = 0 then ∅ else {j h} in
-is_sum_of_is_sum $ assume u, exists.intro (ii u) $
+has_sum_of_has_sum $ assume u, exists.intro (ii u) $
   assume v hv, exists.intro (u ∪ jj v) $ and.intro (subset_union_left _ _) $
   have ∀c:γ, c ∈ u ∪ jj v → c ∉ jj v → g c = 0,
     from assume c hc hnc, classical.by_contradiction $ assume h : g c ≠ 0,
@@ -229,19 +229,19 @@ is_sum_of_is_sum $ assume u, exists.intro (ii u) $
     ... = v.sum _ : sum_bind $ by intros x hx y hy hxy; by_cases f x = 0; by_cases f y = 0; simp [*]
     ... = v.sum f : sum_congr rfl $ by intros x hx; by_cases f x = 0; simp [*]
 
-lemma is_sum_iff_is_sum_of_ne_zero : is_sum f a ↔ is_sum g a :=
+lemma has_sum_iff_has_sum_of_ne_zero : has_sum f a ↔ has_sum g a :=
 iff.intro
-  (is_sum_of_is_sum_ne_zero j hj i hi hij hji $ assume b hb, by rw [←hgj (hi _), hji])
-  (is_sum_of_is_sum_ne_zero i hi j hj hji hij hgj)
+  (has_sum_of_has_sum_ne_zero j hj i hi hij hji $ assume b hb, by rw [←hgj (hi _), hji])
+  (has_sum_of_has_sum_ne_zero i hi j hj hji hij hgj)
 
-lemma has_sum_iff_has_sum_ne_zero : has_sum g ↔ has_sum f :=
+lemma summable_iff_summable_ne_zero : summable g ↔ summable f :=
 exists_congr $
-  assume a, is_sum_iff_is_sum_of_ne_zero j hj i hi hij hji $
+  assume a, has_sum_iff_has_sum_of_ne_zero j hj i hi hij hji $
     assume b hb, by rw [←hgj (hi _), hji]
 
-end is_sum_iff_is_sum_of_iso_ne_zero
+end has_sum_iff_has_sum_of_iso_ne_zero
 
-section is_sum_iff_is_sum_of_bij_ne_zero
+section has_sum_iff_has_sum_of_bij_ne_zero
 variables [add_comm_monoid α] [topological_space α] [topological_add_monoid α]
 variables {f : β → α} {g : γ → α} {a : α}
   (i : Π⦃c⦄, g c ≠ 0 → β)
@@ -250,7 +250,7 @@ variables {f : β → α} {g : γ → α} {a : α}
   (h₃ : ∀⦃c⦄ (h : g c ≠ 0), f (i h) = g c)
 include i h₁ h₂ h₃
 
-lemma is_sum_iff_is_sum_of_ne_zero_bij : is_sum f a ↔ is_sum g a :=
+lemma has_sum_iff_has_sum_of_ne_zero_bij : has_sum f a ↔ has_sum g a :=
 have hi : ∀⦃c⦄ (h : g c ≠ 0), f (i h) ≠ 0,
   from assume c h, by simp [h₃, h],
 let j : Π⦃b⦄, f b ≠ 0 → γ := λb h, some $ h₂ h in
@@ -260,38 +260,38 @@ have hj₁ : ∀⦃b⦄ (h : f b ≠ 0), g (j h) ≠ 0,
   from assume b h, let ⟨h₁, _⟩ := hj h in h₁,
 have hj₂ : ∀⦃b⦄ (h : f b ≠ 0), i (hj₁ h) = b,
   from assume b h, let ⟨h₁, h₂⟩ := hj h in h₂,
-is_sum_iff_is_sum_of_ne_zero i hi j hj₁
+has_sum_iff_has_sum_of_ne_zero i hi j hj₁
   (assume c h, h₁ (hj₁ _) h $ hj₂ _) hj₂ (assume b h, by rw [←h₃ (hj₁ _), hj₂])
 
-lemma has_sum_iff_has_sum_ne_zero_bij : has_sum f ↔ has_sum g :=
+lemma summable_iff_summable_ne_zero_bij : summable f ↔ summable g :=
 exists_congr $
-  assume a, is_sum_iff_is_sum_of_ne_zero_bij @i h₁ h₂ h₃
+  assume a, has_sum_iff_has_sum_of_ne_zero_bij @i h₁ h₂ h₃
 
-end is_sum_iff_is_sum_of_bij_ne_zero
+end has_sum_iff_has_sum_of_bij_ne_zero
 
 section tsum
 variables [add_comm_monoid α] [topological_space α] [topological_add_monoid α] [t2_space α]
 variables {f g : β → α} {a a₁ a₂ : α}
 
-lemma is_sum_unique : is_sum f a₁ → is_sum f a₂ → a₁ = a₂ := tendsto_nhds_unique at_top_ne_bot
+lemma has_sum_unique : has_sum f a₁ → has_sum f a₂ → a₁ = a₂ := tendsto_nhds_unique at_top_ne_bot
 
-lemma tsum_eq_is_sum (ha : is_sum f a) : (∑b, f b) = a := is_sum_unique (is_sum_tsum ⟨a, ha⟩) ha
+lemma tsum_eq_has_sum (ha : has_sum f a) : (∑b, f b) = a := has_sum_unique (has_sum_tsum ⟨a, ha⟩) ha
 
-lemma is_sum_iff_of_has_sum (h : has_sum f) : is_sum f a ↔ (∑b, f b) = a :=
-iff.intro tsum_eq_is_sum (assume eq, eq ▸ is_sum_tsum h)
+lemma has_sum_iff_of_summable (h : summable f) : has_sum f a ↔ (∑b, f b) = a :=
+iff.intro tsum_eq_has_sum (assume eq, eq ▸ has_sum_tsum h)
 
-@[simp] lemma tsum_zero : (∑b:β, 0:α) = 0 := tsum_eq_is_sum is_sum_zero
+@[simp] lemma tsum_zero : (∑b:β, 0:α) = 0 := tsum_eq_has_sum has_sum_zero
 
-lemma tsum_add (hf : has_sum f) (hg : has_sum g) : (∑b, f b + g b) = (∑b, f b) + (∑b, g b) :=
-tsum_eq_is_sum $ is_sum_add (is_sum_tsum hf) (is_sum_tsum hg)
+lemma tsum_add (hf : summable f) (hg : summable g) : (∑b, f b + g b) = (∑b, f b) + (∑b, g b) :=
+tsum_eq_has_sum $ has_sum_add (has_sum_tsum hf) (has_sum_tsum hg)
 
-lemma tsum_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, has_sum (f i)) :
+lemma tsum_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, summable (f i)) :
   (∑b, s.sum (λi, f i b)) = s.sum (λi, ∑b, f i b) :=
-tsum_eq_is_sum $ is_sum_sum $ assume i hi, is_sum_tsum $ hf i hi
+tsum_eq_has_sum $ has_sum_sum $ assume i hi, has_sum_tsum $ hf i hi
 
 lemma tsum_eq_sum {f : β → α} {s : finset β} (hf : ∀b∉s, f b = 0)  :
   (∑b, f b) = s.sum f :=
-tsum_eq_is_sum $ is_sum_sum_of_ne_finset_zero hf
+tsum_eq_has_sum $ has_sum_sum_of_ne_finset_zero hf
 
 lemma tsum_fintype [fintype β] (f : β → α) : (∑b, f b) = finset.univ.sum f :=
 tsum_eq_sum $ λ a h, h.elim (mem_univ _)
@@ -302,21 +302,21 @@ calc (∑b, f b) = (finset.singleton b).sum f : tsum_eq_sum $ by simp [hf] {cont
   ... = f b : by simp
 
 lemma tsum_sigma [regular_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
-  (h₁ : ∀b, has_sum (λc, f ⟨b, c⟩)) (h₂ : has_sum f) : (∑p, f p) = (∑b c, f ⟨b, c⟩):=
-(tsum_eq_is_sum $ is_sum_sigma (assume b, is_sum_tsum $ h₁ b) $ is_sum_tsum h₂).symm
+  (h₁ : ∀b, summable (λc, f ⟨b, c⟩)) (h₂ : summable f) : (∑p, f p) = (∑b c, f ⟨b, c⟩):=
+(tsum_eq_has_sum $ has_sum_sigma (assume b, has_sum_tsum $ h₁ b) $ has_sum_tsum h₂).symm
 
 @[simp] lemma tsum_ite_eq (b : β) (a : α) : (∑b', if b' = b then a else 0) = a :=
-tsum_eq_is_sum (is_sum_ite_eq b a)
+tsum_eq_has_sum (has_sum_ite_eq b a)
 
-lemma tsum_eq_tsum_of_is_sum_iff_is_sum {f : β → α} {g : γ → α}
-  (h : ∀{a}, is_sum f a ↔ is_sum g a) : (∑b, f b) = (∑c, g c) :=
+lemma tsum_eq_tsum_of_has_sum_iff_has_sum {f : β → α} {g : γ → α}
+  (h : ∀{a}, has_sum f a ↔ has_sum g a) : (∑b, f b) = (∑c, g c) :=
 by_cases
-  (assume : ∃a, is_sum f a,
+  (assume : ∃a, has_sum f a,
     let ⟨a, hfa⟩ := this in
-    have hga : is_sum g a, from h.mp hfa,
-    by rw [tsum_eq_is_sum hfa, tsum_eq_is_sum hga])
-  (assume hf : ¬ has_sum f,
-    have hg : ¬ has_sum g, from assume ⟨a, hga⟩, hf ⟨a, h.mpr hga⟩,
+    have hga : has_sum g a, from h.mp hfa,
+    by rw [tsum_eq_has_sum hfa, tsum_eq_has_sum hga])
+  (assume hf : ¬ summable f,
+    have hg : ¬ summable g, from assume ⟨a, hga⟩, hf ⟨a, h.mpr hga⟩,
     by simp [tsum, hf, hg])
 
 lemma tsum_eq_tsum_of_ne_zero {f : β → α} {g : γ → α}
@@ -326,7 +326,7 @@ lemma tsum_eq_tsum_of_ne_zero {f : β → α} {g : γ → α}
   (hij : ∀⦃b⦄ (h : f b ≠ 0), i (hj h) = b)
   (hgj : ∀⦃b⦄ (h : f b ≠ 0), g (j h) = f b) :
   (∑i, f i) = (∑j, g j) :=
-tsum_eq_tsum_of_is_sum_iff_is_sum $ assume a, is_sum_iff_is_sum_of_ne_zero i hi j hj hji hij hgj
+tsum_eq_tsum_of_has_sum_iff_has_sum $ assume a, has_sum_iff_has_sum_of_ne_zero i hi j hj hji hij hgj
 
 lemma tsum_eq_tsum_of_ne_zero_bij {f : β → α} {g : γ → α}
   (i : Π⦃c⦄, g c ≠ 0 → β)
@@ -334,12 +334,12 @@ lemma tsum_eq_tsum_of_ne_zero_bij {f : β → α} {g : γ → α}
   (h₂ : ∀⦃b⦄, f b ≠ 0 → ∃c (h : g c ≠ 0), i h = b)
   (h₃ : ∀⦃c⦄ (h : g c ≠ 0), f (i h) = g c) :
   (∑i, f i) = (∑j, g j) :=
-tsum_eq_tsum_of_is_sum_iff_is_sum $ assume a, is_sum_iff_is_sum_of_ne_zero_bij i h₁ h₂ h₃
+tsum_eq_tsum_of_has_sum_iff_has_sum $ assume a, has_sum_iff_has_sum_of_ne_zero_bij i h₁ h₂ h₃
 
 lemma tsum_eq_tsum_of_iso (j : γ → β) (i : β → γ)
   (h₁ : ∀x, i (j x) = x) (h₂ : ∀x, j (i x) = x) :
   (∑c, f (j c)) = (∑b, f b) :=
-tsum_eq_tsum_of_is_sum_iff_is_sum $ assume a, is_sum_iff_is_sum_of_iso i h₁ h₂
+tsum_eq_tsum_of_has_sum_iff_has_sum $ assume a, has_sum_iff_has_sum_of_iso i h₁ h₂
 
 lemma tsum_equiv (j : γ ≃ β) : (∑c, f (j c)) = (∑b, f b) :=
 tsum_eq_tsum_of_iso j j.symm (by simp) (by simp)
@@ -350,26 +350,26 @@ section topological_group
 variables [add_comm_group α] [topological_space α] [topological_add_group α]
 variables {f g : β → α} {a a₁ a₂ : α}
 
-lemma is_sum_neg : is_sum f a → is_sum (λb, - f b) (- a) :=
-is_sum_hom has_neg.neg continuous_neg'
+lemma has_sum_neg : has_sum f a → has_sum (λb, - f b) (- a) :=
+has_sum_hom has_neg.neg continuous_neg'
 
-lemma has_sum_neg (hf : has_sum f) : has_sum (λb, - f b) :=
-has_sum_spec $ is_sum_neg $ is_sum_tsum $ hf
+lemma summable_neg (hf : summable f) : summable (λb, - f b) :=
+summable_spec $ has_sum_neg $ has_sum_tsum $ hf
 
-lemma is_sum_sub (hf : is_sum f a₁) (hg : is_sum g a₂) : is_sum (λb, f b - g b) (a₁ - a₂) :=
-by simp; exact is_sum_add hf (is_sum_neg hg)
+lemma has_sum_sub (hf : has_sum f a₁) (hg : has_sum g a₂) : has_sum (λb, f b - g b) (a₁ - a₂) :=
+by simp; exact has_sum_add hf (has_sum_neg hg)
 
-lemma has_sum_sub (hf : has_sum f) (hg : has_sum g) : has_sum (λb, f b - g b) :=
-has_sum_spec $ is_sum_sub (is_sum_tsum hf) (is_sum_tsum hg)
+lemma summable_sub (hf : summable f) (hg : summable g) : summable (λb, f b - g b) :=
+summable_spec $ has_sum_sub (has_sum_tsum hf) (has_sum_tsum hg)
 
 section tsum
 variables [t2_space α]
 
-lemma tsum_neg (hf : has_sum f) : (∑b, - f b) = - (∑b, f b) :=
-tsum_eq_is_sum $ is_sum_neg $ is_sum_tsum $ hf
+lemma tsum_neg (hf : summable f) : (∑b, - f b) = - (∑b, f b) :=
+tsum_eq_has_sum $ has_sum_neg $ has_sum_tsum $ hf
 
-lemma tsum_sub (hf : has_sum f) (hg : has_sum g) : (∑b, f b - g b) = (∑b, f b) - (∑b, g b) :=
-tsum_eq_is_sum $ is_sum_sub (is_sum_tsum hf) (is_sum_tsum hg)
+lemma tsum_sub (hf : summable f) (hg : summable g) : (∑b, f b - g b) = (∑b, f b) - (∑b, g b) :=
+tsum_eq_has_sum $ has_sum_sub (has_sum_tsum hf) (has_sum_tsum hg)
 
 end tsum
 
@@ -379,27 +379,27 @@ section topological_semiring
 variables [semiring α] [topological_space α] [topological_semiring α]
 variables {f g : β → α} {a a₁ a₂ : α}
 
-lemma is_sum_mul_left (a₂) : is_sum f a₁ → is_sum (λb, a₂ * f b) (a₂ * a₁) :=
-is_sum_hom _ (continuous_mul continuous_const continuous_id)
+lemma has_sum_mul_left (a₂) : has_sum f a₁ → has_sum (λb, a₂ * f b) (a₂ * a₁) :=
+has_sum_hom _ (continuous_mul continuous_const continuous_id)
 
-lemma is_sum_mul_right (a₂) (hf : is_sum f a₁) : is_sum (λb, f b * a₂) (a₁ * a₂) :=
-@is_sum_hom _ _ _ _ _ _ f a₁ (λa, a * a₂) _ _ _ _
+lemma has_sum_mul_right (a₂) (hf : has_sum f a₁) : has_sum (λb, f b * a₂) (a₁ * a₂) :=
+@has_sum_hom _ _ _ _ _ _ f a₁ (λa, a * a₂) _ _ _ _
   (continuous_mul continuous_id continuous_const) hf
 
-lemma has_sum_mul_left (a) (hf : has_sum f) : has_sum (λb, a * f b) :=
-has_sum_spec $ is_sum_mul_left _ $ is_sum_tsum hf
+lemma summable_mul_left (a) (hf : summable f) : summable (λb, a * f b) :=
+summable_spec $ has_sum_mul_left _ $ has_sum_tsum hf
 
-lemma has_sum_mul_right (a) (hf : has_sum f) : has_sum (λb, f b * a) :=
-has_sum_spec $ is_sum_mul_right _ $ is_sum_tsum hf
+lemma summable_mul_right (a) (hf : summable f) : summable (λb, f b * a) :=
+summable_spec $ has_sum_mul_right _ $ has_sum_tsum hf
 
 section tsum
 variables [t2_space α]
 
-lemma tsum_mul_left (a) (hf : has_sum f) : (∑b, a * f b) = a * (∑b, f b) :=
-tsum_eq_is_sum $ is_sum_mul_left _ $ is_sum_tsum hf
+lemma tsum_mul_left (a) (hf : summable f) : (∑b, a * f b) = a * (∑b, f b) :=
+tsum_eq_has_sum $ has_sum_mul_left _ $ has_sum_tsum hf
 
-lemma tsum_mul_right (a) (hf : has_sum f) : (∑b, f b * a) = (∑b, f b) * a :=
-tsum_eq_is_sum $ is_sum_mul_right _ $ is_sum_tsum hf
+lemma tsum_mul_right (a) (hf : summable f) : (∑b, f b * a) = (∑b, f b) * a :=
+tsum_eq_has_sum $ has_sum_mul_right _ $ has_sum_tsum hf
 
 end tsum
 
@@ -410,15 +410,15 @@ variables [ordered_comm_monoid α] [topological_space α] [ordered_topology α]
   [topological_add_monoid α]
 variables {f g : β → α} {a a₁ a₂ : α}
 
-lemma is_sum_le (h : ∀b, f b ≤ g b) (hf : is_sum f a₁) (hg : is_sum g a₂) : a₁ ≤ a₂ :=
+lemma has_sum_le (h : ∀b, f b ≤ g b) (hf : has_sum f a₁) (hg : has_sum g a₂) : a₁ ≤ a₂ :=
 le_of_tendsto_of_tendsto at_top_ne_bot hf hg $ univ_mem_sets' $
   assume s, sum_le_sum' $ assume b _, h b
 
-lemma is_sum_le_inj {g : γ → α} (i : β → γ) (hi : injective i) (hs : ∀c∉set.range i, 0 ≤ g c)
-  (h : ∀b, f b ≤ g (i b)) (hf : is_sum f a₁) (hg : is_sum g a₂) : a₁ ≤ a₂ :=
-have is_sum (λc, (partial_inv i c).cases_on' 0 f) a₁,
+lemma has_sum_le_inj {g : γ → α} (i : β → γ) (hi : injective i) (hs : ∀c∉set.range i, 0 ≤ g c)
+  (h : ∀b, f b ≤ g (i b)) (hf : has_sum f a₁) (hg : has_sum g a₂) : a₁ ≤ a₂ :=
+have has_sum (λc, (partial_inv i c).cases_on' 0 f) a₁,
 begin
-  refine (is_sum_iff_is_sum_of_ne_zero_bij (λb _, i b) _ _ _).2 hf,
+  refine (has_sum_iff_has_sum_of_ne_zero_bij (λb _, i b) _ _ _).2 hf,
   { assume c₁ c₂ h₁ h₂ eq, exact hi eq },
   { assume c hc,
     cases eq : partial_inv i c with b; rw eq at hc,
@@ -428,7 +428,7 @@ begin
   { assume c hc, rw [partial_inv_left hi, option.cases_on'] }
 end,
 begin
-  refine is_sum_le (assume c, _) this hg,
+  refine has_sum_le (assume c, _) this hg,
   by_cases c ∈ set.range i,
   { rcases h with ⟨b, rfl⟩,
     rw [partial_inv_left hi, option.cases_on'],
@@ -438,8 +438,8 @@ begin
     exact hs _ h }
 end
 
-lemma tsum_le_tsum (h : ∀b, f b ≤ g b) (hf : has_sum f) (hg : has_sum g) : (∑b, f b) ≤ (∑b, g b) :=
-is_sum_le h (is_sum_tsum hf) (is_sum_tsum hg)
+lemma tsum_le_tsum (h : ∀b, f b ≤ g b) (hf : summable f) (hg : summable g) : (∑b, f b) ≤ (∑b, g b) :=
+has_sum_le h (has_sum_tsum hf) (has_sum_tsum hg)
 
 end order_topology
 
@@ -448,13 +448,13 @@ section uniform_group
 variables [add_comm_group α] [uniform_space α] [complete_space α] [uniform_add_group α]
 variables (f g : β → α) {a a₁ a₂ : α}
 
-lemma has_sum_iff_cauchy : has_sum f ↔ cauchy (map (λ (s : finset β), sum s f) at_top) :=
+lemma summable_iff_cauchy : summable f ↔ cauchy (map (λ (s : finset β), sum s f) at_top) :=
 (cauchy_map_iff_exists_tendsto at_top_ne_bot).symm
 
-lemma has_sum_iff_vanishing :
-  has_sum f ↔ ∀ e ∈ nhds (0:α), (∃s:finset β, ∀t, disjoint t s → t.sum f ∈ e) :=
+lemma summable_iff_vanishing :
+  summable f ↔ ∀ e ∈ nhds (0:α), (∃s:finset β, ∀t, disjoint t s → t.sum f ∈ e) :=
 begin
-  simp only [has_sum_iff_cauchy, cauchy_map_iff, and_iff_right at_top_ne_bot,
+  simp only [summable_iff_cauchy, cauchy_map_iff, and_iff_right at_top_ne_bot,
     prod_at_top_at_top_eq, uniformity_eq_comap_nhds_zero α, tendsto_comap_iff, (∘)],
   rw [tendsto_at_top' (_ : finset β × finset β → α)],
   split,
@@ -478,10 +478,10 @@ begin
 end
 
 /- TODO: generalize to monoid with a uniform continuous subtraction operator: `(a + b) - b = a` -/
-lemma has_sum_of_has_sum_of_sub (hf : has_sum f) (h : ∀b, g b = 0 ∨ g b = f b) : has_sum g :=
-(has_sum_iff_vanishing g).2 $
+lemma summable_of_summable_of_sub (hf : summable f) (h : ∀b, g b = 0 ∨ g b = f b) : summable g :=
+(summable_iff_vanishing g).2 $
   assume e he,
-  let ⟨s, hs⟩ := (has_sum_iff_vanishing f).1 hf e he in
+  let ⟨s, hs⟩ := (summable_iff_vanishing f).1 hf e he in
   ⟨s, assume t ht,
     have eq : (t.filter (λb, g b = f b)).sum f = t.sum g :=
       calc (t.filter (λb, g b = f b)).sum f = (t.filter (λb, g b = f b)).sum g :
@@ -495,11 +495,11 @@ lemma has_sum_of_has_sum_of_sub (hf : has_sum f) (h : ∀b, g b = 0 ∨ g b = f
         end,
     eq ▸ hs _ $ finset.disjoint_of_subset_left (finset.filter_subset _) ht⟩
 
-lemma has_sum_comp_of_has_sum_of_injective {i : γ → β} (hf : has_sum f) (hi : injective i) :
-  has_sum (f ∘ i) :=
-suffices has_sum (λb, if b ∈ set.range i then f b else 0),
+lemma summable_comp_of_summable_of_injective {i : γ → β} (hf : summable f) (hi : injective i) :
+  summable (f ∘ i) :=
+suffices summable (λb, if b ∈ set.range i then f b else 0),
 begin
-  refine (has_sum_iff_has_sum_ne_zero_bij (λc _, i c) _ _ _).1 this,
+  refine (summable_iff_summable_ne_zero_bij (λc _, i c) _ _ _).1 this,
   { assume c₁ c₂ hc₁ hc₂ eq, exact hi eq },
   { assume b hb,
     split_ifs at hb,
@@ -508,19 +508,19 @@ begin
     { contradiction } },
   { assume c hc, exact if_pos (set.mem_range_self _) }
 end,
-has_sum_of_has_sum_of_sub _ _ hf $ assume b, by by_cases b ∈ set.range i; simp [h]
+summable_of_summable_of_sub _ _ hf $ assume b, by by_cases b ∈ set.range i; simp [h]
 
 end uniform_group
 
 section cauchy_seq
 open finset.Ico filter
 
-lemma cauchy_seq_of_has_sum_dist [metric_space α] {f : ℕ → α}
-  (h : has_sum (λn, dist (f n) (f n.succ))) : cauchy_seq f :=
+lemma cauchy_seq_of_summable_dist [metric_space α] {f : ℕ → α}
+  (h : summable (λn, dist (f n) (f n.succ))) : cauchy_seq f :=
 begin
   let d := λn, dist (f n) (f (n+1)),
   refine metric.cauchy_seq_iff'.2 (λε εpos, _),
-  rcases (has_sum_iff_vanishing _).1 h {x : ℝ | x < ε} (gt_mem_nhds εpos) with ⟨s, hs⟩,
+  rcases (summable_iff_vanishing _).1 h {x : ℝ | x < ε} (gt_mem_nhds εpos) with ⟨s, hs⟩,
   have : ∃N:ℕ, ∀x ∈ s, x < N,
   { by_cases h : s = ∅,
     { use 0, simp [h]},
diff --git a/src/topology/instances/ennreal.lean b/src/topology/instances/ennreal.lean
index f767c30ae8fca..063380dfa8971 100644
--- a/src/topology/instances/ennreal.lean
+++ b/src/topology/instances/ennreal.lean
@@ -296,19 +296,19 @@ section tsum
 
 variables {f g : α → ennreal}
 
-protected lemma is_sum_coe {f : α → nnreal} {r : nnreal} :
-  is_sum (λa, (f a : ennreal)) ↑r ↔ is_sum f r :=
+protected lemma has_sum_coe {f : α → nnreal} {r : nnreal} :
+  has_sum (λa, (f a : ennreal)) ↑r ↔ has_sum f r :=
 have (λs:finset α, s.sum (coe ∘ f)) = (coe : nnreal → ennreal) ∘ (λs:finset α, s.sum f),
   from funext $ assume s, ennreal.coe_finset_sum.symm,
-by unfold is_sum; rw [this, tendsto_coe]
+by unfold has_sum; rw [this, tendsto_coe]
 
-protected lemma tsum_coe_eq {f : α → nnreal} (h : is_sum f r) : (∑a, (f a : ennreal)) = r :=
-tsum_eq_is_sum $ ennreal.is_sum_coe.2 $ h
+protected lemma tsum_coe_eq {f : α → nnreal} (h : has_sum f r) : (∑a, (f a : ennreal)) = r :=
+tsum_eq_has_sum $ ennreal.has_sum_coe.2 $ h
 
-protected lemma tsum_coe {f : α → nnreal} : has_sum f → (∑a, (f a : ennreal)) = ↑(tsum f)
-| ⟨r, hr⟩ := by rw [tsum_eq_is_sum hr, ennreal.tsum_coe_eq hr]
+protected lemma tsum_coe {f : α → nnreal} : summable f → (∑a, (f a : ennreal)) = ↑(tsum f)
+| ⟨r, hr⟩ := by rw [tsum_eq_has_sum hr, ennreal.tsum_coe_eq hr]
 
-protected lemma is_sum : is_sum f (⨆s:finset α, s.sum f) :=
+protected lemma has_sum : has_sum f (⨆s:finset α, s.sum f) :=
 tendsto_orderable.2
   ⟨assume a' ha',
     let ⟨s, hs⟩ := lt_supr_iff.mp ha' in
@@ -319,14 +319,14 @@ tendsto_orderable.2
       from le_supr (λ(s : finset α), s.sum f) s,
     lt_of_le_of_lt this ha'⟩
 
-@[simp] protected lemma has_sum : has_sum f := ⟨_, ennreal.is_sum⟩
+@[simp] protected lemma summable : summable f := ⟨_, ennreal.has_sum⟩
 
 protected lemma tsum_eq_supr_sum : (∑a, f a) = (⨆s:finset α, s.sum f) :=
-tsum_eq_is_sum ennreal.is_sum
+tsum_eq_has_sum ennreal.has_sum
 
 protected lemma tsum_sigma {β : α → Type*} (f : Πa, β a → ennreal) :
   (∑p:Σa, β a, f p.1 p.2) = (∑a b, f a b) :=
-tsum_sigma (assume b, ennreal.has_sum) ennreal.has_sum
+tsum_sigma (assume b, ennreal.summable) ennreal.summable
 
 protected lemma tsum_prod {f : α → β → ennreal} : (∑p:α×β, f p.1 p.2) = (∑a, ∑b, f a b) :=
 let j : α × β → (Σa:α, β) := λp, sigma.mk p.1 p.2 in
@@ -344,10 +344,10 @@ calc (∑a, ∑b, f a b) = (∑p:α×β, f' p) : ennreal.tsum_prod.symm
   ... = (∑b, ∑a, f' (prod.swap (b, a))) : @ennreal.tsum_prod β α (λb a, f' (prod.swap (b, a)))
 
 protected lemma tsum_add : (∑a, f a + g a) = (∑a, f a) + (∑a, g a) :=
-tsum_add ennreal.has_sum ennreal.has_sum
+tsum_add ennreal.summable ennreal.summable
 
 protected lemma tsum_le_tsum (h : ∀a, f a ≤ g a) : (∑a, f a) ≤ (∑a, g a) :=
-tsum_le_tsum h ennreal.has_sum ennreal.has_sum
+tsum_le_tsum h ennreal.summable ennreal.summable
 
 protected lemma tsum_eq_supr_nat {f : ℕ → ennreal} :
   (∑i:ℕ, f i) = (⨆i:ℕ, (finset.range i).sum f) :=
@@ -372,8 +372,8 @@ have sum_ne_0 : (∑i, f i) ≠ 0, from ne_of_gt $
 have tendsto (λs:finset α, s.sum ((*) a ∘ f)) at_top (nhds (a * (∑i, f i))),
   by rw [← show (*) a ∘ (λs:finset α, s.sum f) = λs, s.sum ((*) a ∘ f),
          from funext $ λ s, finset.mul_sum];
-  exact ennreal.tendsto_mul_right (is_sum_tsum ennreal.has_sum) (or.inl sum_ne_0),
-tsum_eq_is_sum this
+  exact ennreal.tendsto_mul_right (has_sum_tsum ennreal.summable) (or.inl sum_ne_0),
+tsum_eq_has_sum this
 
 protected lemma tsum_mul : (∑i, f i * a) = (∑i, f i) * a :=
 by simp [mul_comm, ennreal.mul_tsum]
@@ -391,12 +391,12 @@ le_antisymm
   (calc f a ≤ (⨆ (h : a = a), f a) : le_supr (λh:a=a, f a) rfl
     ... ≤ (∑b:α, ⨆ (h : a = b), f b) : ennreal.le_tsum _)
 
-lemma is_sum_iff_tendsto_nat {f : ℕ → ennreal} (r : ennreal) :
-  is_sum f r ↔ tendsto (λn:ℕ, (finset.range n).sum f) at_top (nhds r) :=
+lemma has_sum_iff_tendsto_nat {f : ℕ → ennreal} (r : ennreal) :
+  has_sum f r ↔ tendsto (λn:ℕ, (finset.range n).sum f) at_top (nhds r) :=
 begin
-  refine ⟨tendsto_sum_nat_of_is_sum, assume h, _⟩,
+  refine ⟨tendsto_sum_nat_of_has_sum, assume h, _⟩,
   rw [← supr_eq_of_tendsto _ h, ← ennreal.tsum_eq_supr_nat],
-  { exact is_sum_tsum ennreal.has_sum },
+  { exact has_sum_tsum ennreal.summable },
   { exact assume s t hst, finset.sum_le_sum_of_subset (finset.range_subset.2 hst) }
 end
 
@@ -406,41 +406,41 @@ end ennreal
 
 namespace nnreal
 
-lemma exists_le_is_sum_of_le {f g : β → nnreal} {r : nnreal}
-  (hgf : ∀b, g b ≤ f b) (hfr : is_sum f r) : ∃p≤r, is_sum g p :=
+lemma exists_le_has_sum_of_le {f g : β → nnreal} {r : nnreal}
+  (hgf : ∀b, g b ≤ f b) (hfr : has_sum f r) : ∃p≤r, has_sum g p :=
 have (∑b, (g b : ennreal)) ≤ r,
 begin
-  refine is_sum_le (assume b, _) (is_sum_tsum ennreal.has_sum) (ennreal.is_sum_coe.2 hfr),
+  refine has_sum_le (assume b, _) (has_sum_tsum ennreal.summable) (ennreal.has_sum_coe.2 hfr),
   exact ennreal.coe_le_coe.2 (hgf _)
 end,
 let ⟨p, eq, hpr⟩ := ennreal.le_coe_iff.1 this in
-⟨p, hpr, ennreal.is_sum_coe.1 $ eq ▸ is_sum_tsum ennreal.has_sum⟩
+⟨p, hpr, ennreal.has_sum_coe.1 $ eq ▸ has_sum_tsum ennreal.summable⟩
 
-lemma has_sum_of_le {f g : β → nnreal} (hgf : ∀b, g b ≤ f b) : has_sum f → has_sum g
-| ⟨r, hfr⟩ := let ⟨p, _, hp⟩ := exists_le_is_sum_of_le hgf hfr in has_sum_spec hp
+lemma summable_of_le {f g : β → nnreal} (hgf : ∀b, g b ≤ f b) : summable f → summable g
+| ⟨r, hfr⟩ := let ⟨p, _, hp⟩ := exists_le_has_sum_of_le hgf hfr in summable_spec hp
 
-lemma is_sum_iff_tendsto_nat {f : ℕ → nnreal} (r : nnreal) :
-  is_sum f r ↔ tendsto (λn:ℕ, (finset.range n).sum f) at_top (nhds r) :=
+lemma has_sum_iff_tendsto_nat {f : ℕ → nnreal} (r : nnreal) :
+  has_sum f r ↔ tendsto (λn:ℕ, (finset.range n).sum f) at_top (nhds r) :=
 begin
-  rw [← ennreal.is_sum_coe, ennreal.is_sum_iff_tendsto_nat],
+  rw [← ennreal.has_sum_coe, ennreal.has_sum_iff_tendsto_nat],
   simp only [ennreal.coe_finset_sum.symm],
   exact ennreal.tendsto_coe
 end
 
 end nnreal
 
-lemma has_sum_of_nonneg_of_le {f g : β → ℝ}
-  (hg : ∀b, 0 ≤ g b) (hgf : ∀b, g b ≤ f b) (hf : has_sum f) : has_sum g :=
+lemma summable_of_nonneg_of_le {f g : β → ℝ}
+  (hg : ∀b, 0 ≤ g b) (hgf : ∀b, g b ≤ f b) (hf : summable f) : summable g :=
 let f' (b : β) : nnreal := ⟨f b, le_trans (hg b) (hgf b)⟩ in
 let g' (b : β) : nnreal := ⟨g b, hg b⟩ in
-have has_sum f', from nnreal.has_sum_coe.1 hf,
-have has_sum g', from
-  nnreal.has_sum_of_le (assume b, (@nnreal.coe_le (g' b) (f' b)).2 $ hgf b) this,
-show has_sum (λb, g' b : β → ℝ), from nnreal.has_sum_coe.2 this
-
-lemma is_sum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} (hf : ∀i, 0 ≤ f i) (r : ℝ) :
-  is_sum f r ↔ tendsto (λn:ℕ, (finset.range n).sum f) at_top (nhds r) :=
-⟨tendsto_sum_nat_of_is_sum,
+have summable f', from nnreal.summable_coe.1 hf,
+have summable g', from
+  nnreal.summable_of_le (assume b, (@nnreal.coe_le (g' b) (f' b)).2 $ hgf b) this,
+show summable (λb, g' b : β → ℝ), from nnreal.summable_coe.2 this
+
+lemma has_sum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} (hf : ∀i, 0 ≤ f i) (r : ℝ) :
+  has_sum f r ↔ tendsto (λn:ℕ, (finset.range n).sum f) at_top (nhds r) :=
+⟨tendsto_sum_nat_of_has_sum,
   assume hfr,
   have 0 ≤ r := ge_of_tendsto at_top_ne_bot hfr $ univ_mem_sets' $ assume i,
     show 0 ≤ (finset.range i).sum f, from finset.zero_le_sum $ assume i _, hf i,
@@ -448,7 +448,7 @@ lemma is_sum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} (hf : ∀i, 0 ≤ f i)
   have f_eq : f = (λi:ℕ, (f' i : ℝ)) := rfl,
   have r_eq : r = r' := rfl,
   begin
-    rw [f_eq, r_eq, nnreal.is_sum_coe, nnreal.is_sum_iff_tendsto_nat, ← nnreal.tendsto_coe],
+    rw [f_eq, r_eq, nnreal.has_sum_coe, nnreal.has_sum_iff_tendsto_nat, ← nnreal.tendsto_coe],
     simp only [nnreal.sum_coe],
     exact hfr
   end⟩
diff --git a/src/topology/instances/nnreal.lean b/src/topology/instances/nnreal.lean
index 9ea710aa3e6b6..282a0e6f45336 100644
--- a/src/topology/instances/nnreal.lean
+++ b/src/topology/instances/nnreal.lean
@@ -81,19 +81,19 @@ lemma tendsto_sub {f : filter α} {m n : α → nnreal} {r p : nnreal}
   tendsto (λa, m a - n a) f (nhds (r - p)) :=
 tendsto_of_real $ tendsto_sub (tendsto_coe.2 hm) (tendsto_coe.2 hn)
 
-lemma is_sum_coe {f : α → nnreal} {r : nnreal} : is_sum (λa, (f a : ℝ)) (r : ℝ) ↔ is_sum f r :=
-by simp [is_sum, sum_coe.symm, tendsto_coe]
+lemma has_sum_coe {f : α → nnreal} {r : nnreal} : has_sum (λa, (f a : ℝ)) (r : ℝ) ↔ has_sum f r :=
+by simp [has_sum, sum_coe.symm, tendsto_coe]
 
-lemma has_sum_coe {f : α → nnreal} : has_sum (λa, (f a : ℝ)) ↔ has_sum f :=
+lemma summable_coe {f : α → nnreal} : summable (λa, (f a : ℝ)) ↔ summable f :=
 begin
-  simp [has_sum],
+  simp [summable],
   split,
-  exact assume ⟨a, ha⟩, ⟨⟨a, is_sum_le (λa, (f a).2) is_sum_zero ha⟩, is_sum_coe.1 ha⟩,
-  exact assume ⟨a, ha⟩, ⟨a.1, is_sum_coe.2 ha⟩
+  exact assume ⟨a, ha⟩, ⟨⟨a, has_sum_le (λa, (f a).2) has_sum_zero ha⟩, has_sum_coe.1 ha⟩,
+  exact assume ⟨a, ha⟩, ⟨a.1, has_sum_coe.2 ha⟩
 end
 
-lemma tsum_coe {f : α → nnreal} (hf : has_sum f) : (∑a, (f a : ℝ)) = ↑(∑a, f a) :=
-tsum_eq_is_sum $ is_sum_coe.2 $ is_sum_tsum $ hf
+lemma tsum_coe {f : α → nnreal} (hf : summable f) : (∑a, (f a : ℝ)) = ↑(∑a, f a) :=
+tsum_eq_has_sum $ has_sum_coe.2 $ has_sum_tsum $ hf
 
 end coe