Documentation

Mathlib.Data.NNRat.BigOperators

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

source
theorem NNRat.cast_listSum {K : Type u_2} [DivisionSemiring K] [CharZero K] (l : List ℚ≥0) :
↑l.sum = (List.map NNRat.cast l).sum
source
@[deprecated NNRat.cast_listSum (since := "2025-06-30")]
theorem NNRat.coe_list_sum {K : Type u_2} [DivisionSemiring K] [CharZero K] (l : List ℚ≥0) :
↑l.sum = (List.map NNRat.cast l).sum

Alias of NNRat.cast_listSum.

source
theorem NNRat.cast_listProd {K : Type u_2} [DivisionSemiring K] [CharZero K] (l : List ℚ≥0) :
↑l.prod = (List.map NNRat.cast l).prod
source
@[deprecated NNRat.cast_listProd (since := "2025-06-30")]
theorem NNRat.coe_list_prod {K : Type u_2} [DivisionSemiring K] [CharZero K] (l : List ℚ≥0) :
↑l.prod = (List.map NNRat.cast l).prod

Alias of NNRat.cast_listProd.

source
theorem NNRat.cast_multisetSum {K : Type u_2} [DivisionSemiring K] [CharZero K] (s : Multiset ℚ≥0) :
↑s.sum = (Multiset.map NNRat.cast s).sum
source
@[deprecated NNRat.cast_multisetSum (since := "2025-06-30")]
theorem NNRat.coe_multiset_sum {K : Type u_2} [DivisionSemiring K] [CharZero K] (s : Multiset ℚ≥0) :
↑s.sum = (Multiset.map NNRat.cast s).sum

Alias of NNRat.cast_multisetSum.

source
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)
source
@[deprecated NNRat.cast_sum (since := "2025-06-30")]
theorem NNRat.coe_sum {α : Type u_1} {K : Type u_2} [DivisionSemiring K] [CharZero K] (s : Finset α) (f : α → ℚ≥0) :
↑(∑ a ∈ s, f a) = ∑ a ∈ s, ↑(f a)

Alias of NNRat.cast_sum.

source
theorem NNRat.cast_multisetProd {K : Type u_2} [Semifield K] [CharZero K] (s : Multiset ℚ≥0) :
↑s.prod = (Multiset.map NNRat.cast s).prod
source
@[deprecated NNRat.cast_multisetProd (since := "2025-06-30")]
theorem NNRat.coe_multiset_prod {K : Type u_2} [Semifield K] [CharZero K] (s : Multiset ℚ≥0) :
↑s.prod = (Multiset.map NNRat.cast s).prod

Alias of NNRat.cast_multisetProd.

source
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)
source
@[deprecated NNRat.cast_prod (since := "2025-06-30")]
theorem NNRat.coe_prod {α : Type u_1} {K : Type u_2} [Semifield K] [CharZero K] (s : Finset α) (f : α → ℚ≥0) :
↑(∏ a ∈ s, f a) = ∏ a ∈ s, ↑(f a)

Alias of NNRat.cast_prod.

source
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
source
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