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.

source
@[simp, norm_cast]
theorem rat.cast_list_sum {α : Type u_2} [division_ring α] [char_zero α] (s : list ℚ) :
↑(s.sum) = (list.map coe s).sum
source
@[simp, norm_cast]
theorem rat.cast_multiset_sum {α : Type u_2} [division_ring α] [char_zero α] (s : multiset ℚ) :
↑(s.sum) = (multiset.map coe s).sum
source
@[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))
source
@[simp, norm_cast]
theorem rat.cast_list_prod {α : Type u_2} [division_ring α] [char_zero α] (s : list ℚ) :
↑(s.prod) = (list.map coe s).prod
source
@[simp, norm_cast]
theorem rat.cast_multiset_prod {α : Type u_2} [field α] [char_zero α] (s : multiset ℚ) :
↑(s.prod) = (multiset.map coe s).prod
source
@[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))