Zify

📁 Source: Mathlib/Tactic/Zify.lean

Statistics

Metric	Count
Definitions applySimpResultToProp', mkZifyContext, zify, zifyProof	4
Theorems cast_sub_of_add_le, cast_sub_of_lt, natCast_dvd, natCast_eq, natCast_le, natCast_lt, natCast_ne	7
Total	11

Mathlib.Tactic.Zify

Definitions

Name	Category	Theorems
applySimpResultToProp' 📖	CompOp	—
mkZifyContext 📖	CompOp	—
zify 📖	CompOp	—
zifyProof 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natCast_dvd 📖	—	—	—	—	—
natCast_eq 📖	—	—	—	—	—
natCast_le 📖	—	—	—	—	—
natCast_lt 📖	—	—	—	—	—
natCast_ne 📖	—	—	—	—	—

Mathlib.Tactic.Zify.Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_sub_of_add_le 📖	mathematical	—	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	Nat.cast_sub LE.le.trans
cast_sub_of_lt 📖	mathematical	—	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	Nat.cast_sub LT.lt.le

---

← Back to Index