Metamath Proof Explorer
Table of Contents - 6.2.3. Properties of the canonical representation of a rational
- cnumer
- cdenom
- df-numer
- df-denom
- qnumval
- qdenval
- qnumdencl
- qnumcl
- qdencl
- fnum
- fden
- qnumdenbi
- qnumdencoprm
- qeqnumdivden
- qmuldeneqnum
- divnumden
- divdenle
- qnumgt0
- qgt0numnn
- nn0gcdsq
- zgcdsq
- numdensq
- numsq
- densq
- qden1elz
- zsqrtelqelz
- nonsq