mathlib3 documentation

data.rat.big_operators

Casting lemmas for rational numbers involving sums and products #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[simp, norm_cast]
theorem rat.cast_list_sum {α : Type u_2} [division_ring α] [char_zero α] (s : list ) :
@[simp, norm_cast]
theorem rat.cast_multiset_sum {α : Type u_2} [division_ring α] [char_zero α] (s : multiset ) :
@[simp, norm_cast]
theorem rat.cast_sum {ι : Type u_1} {α : Type u_2} [division_ring α] [char_zero α] (s : finset ι) (f : ι ) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
@[simp, norm_cast]
theorem rat.cast_list_prod {α : Type u_2} [division_ring α] [char_zero α] (s : list ) :
@[simp, norm_cast]
theorem rat.cast_multiset_prod {α : Type u_2} [field α] [char_zero α] (s : multiset ) :
@[simp, norm_cast]
theorem rat.cast_prod {ι : Type u_1} {α : Type u_2} [field α] [char_zero α] (s : finset ι) (f : ι ) :
(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), (f i))