Mathlib Map

Theorems · Theorem · number theory

NNRat.num_ne_zero

∀ {q : ℚ≥0}, q.num ≠ 0 ↔ q ≠ 0
Defined in
Mathlib.Data.NNRat.Defs
Cited by
2 results in Mathlib
Foundations
Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

NNRat.den_inv_of_ne_zero · cited by 0NNRat.den_inv_of_ne_zeroNNRat.num_inv_of_ne_zero · cited by 0NNRat.num_inv_of_ne_zeroNNRat · cited by 523NNRatNNRat.num · cited by 53NNRat.numNNRat.num_ne_zeroCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • NNRatstatement and proof · cited by 523
  • NNRat.numstatement · cited by 53

Cited by2

Results whose statement or proof uses this declaration.