Mathlib Map

Theorems · Theorem · number theory

NNRat.cast_id

∀ (n : ℚ≥0), ↑n = n
Defined in
Mathlib.Data.Rat.Init
Cited by
1 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.

eq_nnratCast · cited by 3eq_nnratCastNNRat · cited by 523NNRatNNRat.cast · cited by 235NNRat.castNNRat.cast_idCITED 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 by1

Results whose statement or proof uses this declaration.