Mathlib Map

Theorems · Theorem · number theory

NNRat.ext

∀ {p q : ℚ≥0}, ↑p = ↑q → p = q
Defined in
Mathlib.Data.NNRat.Defs
Cited by
18 results in Mathlib
Foundations
Depth 42 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

NNRat.inv_def · cited by 3NNRat.inv_defNNRat.num_div_den · cited by 3NNRat.num_div_denNNRat.mul_den_eq_num · cited by 2NNRat.mul_den_eq_numRat.toNNRat_mul · cited by 2Rat.toNNRat_mulNNRat.add_def · cited by 1NNRat.add_defNNRat.ext_num_den · cited by 1NNRat.ext_num_denNNRat.toNNRat_coe · cited by 1NNRat.toNNRat_coeNNRat.mul_def · cited by 1NNRat.mul_defNNRat.div_def · cited by 1NNRat.div_defNNRat.num_divNat_den · cited by 1NNRat.num_divNat_denNNRat.cast_divNat · cited by 0NNRat.cast_divNatNNRat.toNNRat_coe_nat · cited by 0NNRat.toNNRat_coe_natRat.toNNRat_add · cited by 0Rat.toNNRat_addNNRat.divNat_eq_div · cited by 0NNRat.divNat_eq_divNNRat.divNat_mul_divNat · cited by 0NNRat.divNat_mul_divNatNNRat · cited by 523NNRatNNRat.cast · cited by 235NNRat.castNNRat.extCITED 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.caststatement · cited by 235

Cited by18

Results whose statement or proof uses this declaration.