Rify

📁 Source: Mathlib/Tactic/Rify.lean

Statistics

Metric	Count
Definitions rify	1
Theorems ofNat_rat_real, ratCast_eq, ratCast_le, ratCast_lt, ratCast_ne	5
Total	6

Mathlib.Tactic.Rify

Definitions

Name	Category	Theorems
rify 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofNat_rat_real 📖	mathematical	—	Real Real.instRatCast	—	—
ratCast_eq 📖	mathematical	—	Real Real.instRatCast	—	IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
ratCast_le 📖	mathematical	—	Real Real.instLE Real.instRatCast	—	Real.instIsStrictOrderedRing
ratCast_lt 📖	mathematical	—	Real Real.instLT Real.instRatCast	—	Real.instIsStrictOrderedRing
ratCast_ne 📖	—	—	—	—	IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing

---

← Back to Index