The sup norm of a nonzero integer point

A point (x, y) of ℤ² other than the origin has max(|x|, |y|) ≥ 1, in any ordered ring the integers are cast to. This is the normalisation behind lower bounds of the form c max(|x|, |y|) ^ e at integer points, as in Liouville- and Roth-type inequalities for binary forms.

theorem Int.one_le_max_abs_cast {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {x y : ℤ} (h : x ≠ 0 ∨ y ≠ 0) : 1 ≤ max |↑x| |↑y|

A point (x, y) of ℤ² other than the origin has max(|x|, |y|) ≥ 1 in every ordered ring R.