Documentation

Mathlib.Data.NNRat.BigOperators

Casting lemmas for non-negative rational numbers involving sums and products #

theorem NNRat.coe_list_sum (l : List ℚ≥0) :
l.sum = (List.map NNRat.cast l).sum
theorem NNRat.coe_list_prod (l : List ℚ≥0) :
l.prod = (List.map NNRat.cast l).prod
theorem NNRat.coe_multiset_sum (s : Multiset ℚ≥0) :
s.sum = (Multiset.map NNRat.cast s).sum
theorem NNRat.coe_multiset_prod (s : Multiset ℚ≥0) :
s.prod = (Multiset.map NNRat.cast s).prod
theorem NNRat.coe_sum {α : Type u_2} {s : Finset α} {f : αℚ≥0} :
(∑ as, f a) = as, (f a)
theorem NNRat.toNNRat_sum_of_nonneg {α : Type u_2} {s : Finset α} {f : α} (hf : as, 0 f a) :
(∑ as, f a).toNNRat = as, (f a).toNNRat
theorem NNRat.coe_prod {α : Type u_2} {s : Finset α} {f : αℚ≥0} :
(∏ as, f a) = as, (f a)
theorem NNRat.toNNRat_prod_of_nonneg {α : Type u_2} {s : Finset α} {f : α} (hf : as, 0 f a) :
(∏ as, f a).toNNRat = as, (f a).toNNRat