Mathlib Map

Theorems · Theorem · number theory

Num.cast_toZNum

∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α] [inst_3 : Neg α] (n : Num), ↑n.toZNum = ↑n
Defined in
Mathlib.Data.Num.Lemmas
Cited by
3 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
ZeroOneAddNeg
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_auxZNum.mod_to_int · cited by 1ZNum.mod_to_intZNum.div_to_int · cited by 0ZNum.div_to_intPosNum · cited by 171PosNumNum · cited by 117NumcastNum · cited by 72castNumcastZNum · cited by 41castZNumNum.toZNum · cited by 18Num.toZNumNum.cast_toZNumCITED BYCITES

Cites5

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

  • PosNumproof · cited by 171
  • Numstatement and proof · cited by 117
  • castNumstatement and proof · cited by 72
  • castZNumstatement and proof · cited by 41
  • Num.toZNumstatement and proof · cited by 18

Cited by3

Results whose statement or proof uses this declaration.