# Casting lemmas for rational numbers involving sums and products #

source
@[simp]
theorem Rat.cast_list_sum {α : Type u_2} [DivisionRing α] [CharZero α] (s : List ℚ) :
↑s.sum = (List.map Rat.cast s).sum
source
@[simp]
theorem Rat.cast_multiset_sum {α : Type u_2} [DivisionRing α] [CharZero α] (s : Multiset ℚ) :
↑s.sum = (Multiset.map Rat.cast s).sum
source
@[simp]
theorem Rat.cast_sum {ι : Type u_1} {α : Type u_2} [DivisionRing α] [CharZero α] (s : Finset ι) (f : ι → ℚ) :
↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
source
@[simp]
theorem Rat.cast_list_prod {α : Type u_2} [DivisionRing α] [CharZero α] (s : List ℚ) :
↑s.prod = (List.map Rat.cast s).prod
source
@[simp]
theorem Rat.cast_multiset_prod {α : Type u_2} [Field α] [CharZero α] (s : Multiset ℚ) :
↑s.prod = (Multiset.map Rat.cast s).prod
source
@[simp]
theorem Rat.cast_prod {ι : Type u_1} {α : Type u_2} [Field α] [CharZero α] (s : Finset ι) (f : ι → ℚ) :
↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)