Documentation
Mathlib
.
Data
.
NNRat
.
BigOperators
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.NNRat.Defs
Mathlib.Algebra.Order.BigOperators.Ring.Finset
Imported by
NNRat
.
coe_list_sum
NNRat
.
coe_list_prod
NNRat
.
coe_multiset_sum
NNRat
.
coe_multiset_prod
NNRat
.
coe_sum
NNRat
.
toNNRat_sum_of_nonneg
NNRat
.
coe_prod
NNRat
.
toNNRat_prod_of_nonneg
Casting lemmas for non-negative rational numbers involving sums and products
#
source
theorem
NNRat
.
coe_list_sum
(l :
List
ℚ≥0
)
:
↑
l
.sum
=
(
List.map
NNRat.cast
l
)
.sum
source
theorem
NNRat
.
coe_list_prod
(l :
List
ℚ≥0
)
:
↑
l
.prod
=
(
List.map
NNRat.cast
l
)
.prod
source
theorem
NNRat
.
coe_multiset_sum
(s :
Multiset
ℚ≥0
)
:
↑
s
.sum
=
(
Multiset.map
NNRat.cast
s
)
.sum
source
theorem
NNRat
.
coe_multiset_prod
(s :
Multiset
ℚ≥0
)
:
↑
s
.prod
=
(
Multiset.map
NNRat.cast
s
)
.prod
source
theorem
NNRat
.
coe_sum
{α :
Type
u_2}
{s :
Finset
α
}
{f :
α
→
ℚ≥0
}
:
↑
(∑
a
∈
s
,
f
a
)
=
∑
a
∈
s
,
↑
(
f
a
)
source
theorem
NNRat
.
toNNRat_sum_of_nonneg
{α :
Type
u_2}
{s :
Finset
α
}
{f :
α
→
ℚ
}
(hf :
∀
a
∈
s
,
0
≤
f
a
)
:
(∑
a
∈
s
,
f
a
)
.toNNRat
=
∑
a
∈
s
,
(
f
a
)
.toNNRat
source
theorem
NNRat
.
coe_prod
{α :
Type
u_2}
{s :
Finset
α
}
{f :
α
→
ℚ≥0
}
:
↑
(∏
a
∈
s
,
f
a
)
=
∏
a
∈
s
,
↑
(
f
a
)
source
theorem
NNRat
.
toNNRat_prod_of_nonneg
{α :
Type
u_2}
{s :
Finset
α
}
{f :
α
→
ℚ
}
(hf :
∀
a
∈
s
,
0
≤
f
a
)
:
(∏
a
∈
s
,
f
a
)
.toNNRat
=
∏
a
∈
s
,
(
f
a
)
.toNNRat