A lower bound from a natural reciprocal below one #
A nonzero natural number whose reciprocal, cast into a preordered division semiring, is less than one is at least two. This converts the reciprocal-sum hypothesis for a hyperbolic triangle group into the parameter bounds needed for its trigonometric matrix representation.
theorem
TauCeti.two_le_of_cast_inv_lt_one
{α : Type u_1}
[DivisionSemiring α]
[Preorder α]
{p : ℕ}
(hp : p ≠ 0)
(h : (↑p)⁻¹ < 1)
:
A nonzero natural number whose reciprocal is less than one is at least two.