Basic

📁 Source: Mathlib/Data/Int/Cast/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems cast_add, cast_four, cast_ite, cast_natCast, cast_neg, cast_negOfNat, cast_negSucc, cast_ofNat, cast_one, cast_sub, cast_subNatNat, cast_three, cast_two, cast_zero, cast_pred, cast_sub, zsmul_one	17
Total	17

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_add 📖	mathematical	—	AddGroupWithOne.toIntCast AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne	—	cast_natCast Nat.cast_add cast_subNatNat cast_negSucc sub_eq_add_neg sub_eq_iff_eq_add add_assoc eq_neg_add_iff_add_eq neg_add_rev
cast_four 📖	mathematical	—	AddGroupWithOne.toIntCast instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	cast_ofNat Nat.instAtLeastTwoHAddOfNat
cast_ite 📖	—	—	—	—	—
cast_natCast 📖	mathematical	—	AddGroupWithOne.toIntCast AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	AddGroupWithOne.intCast_ofNat
cast_neg 📖	mathematical	—	AddGroupWithOne.toIntCast NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddGroupWithOne.toAddGroup	—	cast_zero neg_zero cast_natCast cast_negSucc Nat.cast_add Nat.cast_one neg_add_rev neg_neg
cast_negOfNat 📖	mathematical	—	AddGroupWithOne.toIntCast NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	cast_neg cast_natCast
cast_negSucc 📖	mathematical	—	AddGroupWithOne.toIntCast NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	AddGroupWithOne.intCast_negSucc
cast_ofNat 📖	mathematical	—	AddGroupWithOne.toIntCast	—	AddGroupWithOne.intCast_ofNat
cast_one 📖	mathematical	—	AddGroupWithOne.toIntCast AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	cast_natCast Nat.cast_one
cast_sub 📖	mathematical	—	AddGroupWithOne.toIntCast SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	cast_add cast_neg sub_eq_add_neg
cast_subNatNat 📖	mathematical	—	AddGroupWithOne.toIntCast SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	cast_natCast Nat.cast_sub cast_negSucc le_of_lt neg_sub
cast_three 📖	mathematical	—	AddGroupWithOne.toIntCast instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	cast_ofNat Nat.instAtLeastTwoHAddOfNat
cast_two 📖	mathematical	—	AddGroupWithOne.toIntCast instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	cast_ofNat Nat.instAtLeastTwoHAddOfNat
cast_zero 📖	mathematical	—	AddGroupWithOne.toIntCast NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddGroupWithOne.toAddGroup	—	AddGroupWithOne.intCast_ofNat Nat.cast_zero

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_pred 📖	mathematical	—	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toOne	—	cast_succ add_sub_cancel_right
cast_sub 📖	mathematical	—	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	eq_sub_of_add_eq cast_add

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
zsmul_one 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddGroupWithOne.toIntCast	—	natCast_zsmul nsmul_one Int.cast_natCast negSucc_zsmul Nat.cast_add Nat.cast_one neg_add_rev Int.cast_negSucc

---

← Back to Index