Mathlib Map

Theorems · Definition · number theory

Num.toZNum

Num → ZNum

Converts a Num to a ZNum.

Defined in
Mathlib.Data.Num.Basic
Cited by
18 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ZNum.pred · cited by 5ZNum.predZNum.ofInt' · cited by 5ZNum.ofInt'Num.toZNum_succ · cited by 3Num.toZNum_succNum.zneg_toZNumNeg · cited by 3Num.zneg_toZNumNegNum.cast_toZNum · cited by 3Num.cast_toZNumZNum.of_to_int' · cited by 2ZNum.of_to_int'Num.zneg_toZNum · cited by 2Num.zneg_toZNumNum.ofInt'_toZNum · cited by 1Num.ofInt'_toZNumZNum.zneg_succ · cited by 1ZNum.zneg_succNum.pred_succ · cited by 1Num.pred_succZNum.div · cited by 1ZNum.divZNum.ofInt'_eq · cited by 1ZNum.ofInt'_eqZNum.ofInt'_neg · cited by 1ZNum.ofInt'_negNum.mem_ofZNum' · cited by 1Num.mem_ofZNum'ZNum.of_nat_toZNum · cited by 1ZNum.of_nat_toZNumPosNum · cited by 171PosNumNum · cited by 117NumZNum · cited by 73ZNumNum.toZNumCITED BYCITES

Cites3

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
  • ZNumstatement and proof · cited by 73

Cited by22

Results whose statement or proof uses this declaration.