The circular order on ZMod n

This file defines the circular order on ZMod n.

instance instCircularOrderInt : CircularOrder ℤ

Equations

• instCircularOrderInt = LinearOrder.toCircularOrder ℤ

theorem Int.btw_iff {a b c : ℤ} : btw a b c ↔ a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b

theorem Int.sbtw_iff {a b c : ℤ} : sbtw a b c ↔ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b

instance instCircularOrderFin (n : ℕ) : CircularOrder (Fin n)

Equations

• instCircularOrderFin n = LinearOrder.toCircularOrder (Fin n)

theorem Fin.btw_iff {n : ℕ} {a b c : Fin n} : btw a b c ↔ a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b

theorem Fin.sbtw_iff {n : ℕ} {a b c : Fin n} : sbtw a b c ↔ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b

instance instCircularOrderZMod (n : ℕ) : CircularOrder (ZMod n)

Equations

• instCircularOrderZMod 0 = inferInstanceAs (CircularOrder ℤ)
• instCircularOrderZMod n.succ = inferInstanceAs (CircularOrder (Fin (n + 1)))