rat.cast_sum

Stream: Is there code for X?

[Moritz Firsching]

When considering limits of finite sums of rational numbers, which might converge to some non-rational real number, I was expecting to find rat.cast_sum, having found nat.cast_sum and int.cast_sum

Would something like the following be a useful to have in mathlib?

import tactic
open_locale big_operators
universes u v w
variables {β : Type u} {α : Type v} {γ : Type w}

@[simp, norm_cast] lemma rat.cast_sum [division_ring β] [char_zero β] (s : finset α) (f : α → ℚ) :
  ↑(∑ x in s, (f x : ℚ)) = ∑ x in s, (f x : β) :=
  (rat.cast_hom β).map_sum f s

[Yaël Dillies]

Oh wait I have it on a branch ready to PR and... I didn't open it.

[Eric Wieser]

Indeed

[Yaël Dillies]

Exam time really do be emptying your mind, huh

[Moritz Firsching]

Yaël Dillies said:

Oh wait I have it on a branch ready to PR and... I didn't open it.

Nice! Do you plan to open the PR soon?

[Yaël Dillies]

#14824, sorry for the month delay!

[Stuart Presnell]

Yaël, are you trying to develop a reputation as the Gauss of mathlib? :smile: