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

theorem NNRat.cast_listSum {K : Type u_2} [DivisionSemiring K] [CharZero K] (l : List ℚ≥0) : ↑l.sum = (List.map NNRat.cast l).sum

theorem NNRat.cast_listProd {K : Type u_2} [DivisionSemiring K] [CharZero K] (l : List ℚ≥0) : ↑l.prod = (List.map NNRat.cast l).prod

theorem NNRat.cast_multisetSum {K : Type u_2} [DivisionSemiring K] [CharZero K] (s : Multiset ℚ≥0) : ↑s.sum = (Multiset.map NNRat.cast s).sum

theorem NNRat.cast_sum {α : Type u_1} {K : Type u_2} [DivisionSemiring K] [CharZero K] (s : Finset α) (f : α → ℚ≥0) : ↑(∑ a ∈ s, f a) = ∑ a ∈ s, ↑(f a)

theorem NNRat.cast_multisetProd {K : Type u_2} [Semifield K] [CharZero K] (s : Multiset ℚ≥0) : ↑s.prod = (Multiset.map NNRat.cast s).prod

theorem NNRat.cast_prod {α : Type u_1} {K : Type u_2} [Semifield K] [CharZero K] (s : Finset α) (f : α → ℚ≥0) : ↑(∏ a ∈ s, f a) = ∏ a ∈ s, ↑(f a)

theorem NNRat.toNNRat_sum_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℚ} (hf : ∀ a ∈ s, 0 ≤ f a) : (∑ a ∈ s, f a).toNNRat = ∑ a ∈ s, (f a).toNNRat

theorem NNRat.toNNRat_prod_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℚ} (hf : ∀ a ∈ s, 0 ≤ f a) : (∏ a ∈ s, f a).toNNRat = ∏ a ∈ s, (f a).toNNRat