Theorems · Definition · number theory
castZNum
{α : Type u_1} → [Zero α] → [One α] → [Add α] → [Neg α] → ZNum → αcastZNum casts a ZNum into any type which has 0, 1, + and neg
- Defined in
- Mathlib.Data.Num.Basic
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PosNumproof · cited by 171
- castPosNumproof · cited by 74
- ZNumstatement and proof · cited by 73
Cited by41
Results whose statement or proof uses this declaration.
- ZNum.cast_negstatement · cited by 5
- ZNum.cast_posstatement · cited by 5
- ZNum.cast_to_intstatement and proof · cited by 5
- ZNum.cast_addstatement and proof · cited by 3
- Num.cast_sub'statement and proof · cited by 3
- Num.cast_toZNumstatement and proof · cited by 3
- ZNum.to_int_injstatement and proof · cited by 3
- Num.ofZNum_toNatstatement and proof · cited by 2
- ZNum.cast_znegstatement and proof · cited by 2
- ZNum.lt_to_intstatement and proof · cited by 2
- PosNum.cast_sub'statement · cited by 2
- ZNum.mul_to_intstatement and proof · cited by 2