Mathlib Map

Theorems · Theorem · number theory

Num.to_of_nat

∀ (n : ℕ), ↑↑n = n
Defined in
Mathlib.Data.Num.Lemmas
Cited by
4 results in Mathlib
Foundations
Depth 48 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

PosNum.divMod_to_nat_aux · cited by 1PosNum.divMod_to_nat_auxNum.of_nat_inj · cited by 0Num.of_nat_injComputability.decode_encodeNat · cited by 0Computability.decode_enco…Num.of_natCast · cited by 0Num.of_natCastNum · cited by 117NumcastNum · cited by 72castNumNum.to_of_natCITED BYCITES

Cites2

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

  • Numstatement · cited by 117
  • castNumstatement · cited by 72

Cited by4

Results whose statement or proof uses this declaration.