Documentation
LeanAPAP
.
Mathlib
.
Data
.
NNRat
.
Lemmas
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.NNRat.Lemmas
Imported by
NNRat
.
mul_den_eq_num
NNRat
.
den_mul_eq_num
source
theorem
NNRat
.
mul_den_eq_num
(q :
ℚ≥0
)
:
q
*
↑
q
.den
=
↑
q
.num
source
theorem
NNRat
.
den_mul_eq_num
(q :
ℚ≥0
)
:
↑
q
.den
*
q
=
↑
q
.num