Documentation

Mathlib.Data.Rat.BigOperators

Casting lemmas for rational numbers involving sums and products #

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