Intervals of integers in strict ordered rings #
These statements could perhaps be generalized, or there could be other variations provided (e.g.,
for ℕ instead of ℤ, or a version for locally finite SuccOrders with strictly monotone
functions), but for now these are the ones that have found utility in practice (e.g., for lemmas
about Real.Angle).
theorem
IsStrictOrderedRing.int_mem_Icc_of_mul_mem_Ioo
{R : Type u_1}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{r : R}
(hr : 0 < r)
{k m n : ℤ}
(h : r * ↑k ∈ Set.Ioo (r * ↑(m - 1)) (r * ↑(n + 1)))
:
Let k : ℤ. If its multiple of r > 0 in a strict ordered ring lies strictly between
multiples r * (m - 1) and r * (n + 1), then m ≤ k ≤ n.
theorem
IsStrictOrderedRing.int_eq_of_mul_mem_Ioo
{R : Type u_1}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{r : R}
(hr : 0 < r)
{k m : ℤ}
(h : r * ↑k ∈ Set.Ioo (r * ↑(m - 1)) (r * ↑(m + 1)))
:
Let k : ℤ. If its multiple of r > 0 in a strict ordered ring lies strictly between
the preceding and succeeding multiples r * (m - 1) and r * (m + 1), then k = m.