Theorems · Definition · number theory
Rat.toNNRat
ℚ → ℚ≥0
Reinterpret a rational number q as a non-negative rational number. Returns 0 if q ≤ 0.
- Defined in
- Mathlib.Data.NNRat.Defs
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NNRatstatement · cited by 523
Cited by30
Results whose statement or proof uses this declaration.
- Rat.coe_toNNRatstatement · cited by 6
- Rat.toNNRat_eq_zerostatement and proof · cited by 4
- Rat.toNNRat_invstatement and proof · cited by 2
- Rat.toNNRat_lt_toNNRat_iff'statement · cited by 2
- Rat.toNNRat_mulstatement and proof · cited by 2
- NNRat.gistatement · cited by 2
- Rat.toNNRat_posstatement · cited by 1
- NNRat.toNNRat_coestatement · cited by 1
- Rat.le_toNNRat_iff_coe_lestatement · cited by 1
- NNRat.bddAbove_coeproof · cited by 0
- Rat.lt_toNNRat_iff_coe_ltstatement · cited by 0
- Rat.toNNRat_addstatement · cited by 0