ZMod

📁 Source: Mathlib/Order/Circular/ZMod.lean

Statistics

Metric	Count
Definitions instCircularOrderFin, instCircularOrderInt, instCircularOrderZMod	3
Theorems btw_iff, sbtw_iff, btw_iff, sbtw_iff	4
Total	7

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
btw_iff 📖	mathematical	—	Btw.btw CircularPreorder.toBtw CircularPartialOrder.toCircularPreorder CircularOrder.toCircularPartialOrder instCircularOrderFin	—	—
sbtw_iff 📖	mathematical	—	SBtw.sbtw CircularPreorder.toSBtw CircularPartialOrder.toCircularPreorder CircularOrder.toCircularPartialOrder instCircularOrderFin	—	—

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
btw_iff 📖	mathematical	—	Btw.btw CircularPreorder.toBtw CircularPartialOrder.toCircularPreorder CircularOrder.toCircularPartialOrder instCircularOrderInt	—	—
sbtw_iff 📖	mathematical	—	SBtw.sbtw CircularPreorder.toSBtw CircularPartialOrder.toCircularPreorder CircularOrder.toCircularPartialOrder instCircularOrderInt	—	—

(root)

Definitions

Name	Category	Theorems
instCircularOrderFin 📖	CompOp	2 math math: Fin.sbtw_iff, Fin.btw_iff
instCircularOrderInt 📖	CompOp	2 math math: Int.btw_iff, Int.sbtw_iff
instCircularOrderZMod 📖	CompOp	—

---

← Back to Index