coe summable

Stream: Is there code for X?

[Chris Birkbeck]

Do we have the following:

lemma coe_summable { α : Type*} (f : α → ℝ) : summable ((coe : ℝ → ℂ) ∘ f) ↔ summable f :=

It seems like it must be somewhere but I can't find it.

[Eric Wieser]

Does it fall out as a special case of something like docs#summable.mapL?

[Eric Wieser]

Aha, docs#summable.map_iff_of_left_inverse, which I added a little while back

[Kyle Miller]

That works:

import topology.algebra.infinite_sum
import analysis.complex.basic

lemma coe_summable { α : Type*} (f : α → ℝ) :
  summable ((coe : ℝ → ℂ) ∘ f) ↔ summable f :=
begin
  apply summable.map_iff_of_left_inverse complex.of_real complex.re_add_group_hom,
  exact complex.continuous_of_real,
  exact complex.continuous_re,
  intro, refl,
end

[Chris Birkbeck]

Oh great thanks!

[Chris Birkbeck]

I swear I looked at that file for ages, but couldn't see this!

[Eric Wieser]

I've PR'd this in #18376 as complex.summable_of_real