Commit 2021-06-23 01:21 0bc09d9a
View on Github →feat(algebra/ordered_field): a few monotonicity results for powers (#8022)
This PR proves the monotonicity (strict and non-strict) of n → 1 / a ^ n, for a fixed a < 1 in a linearly ordered field. These are lemmas extracted from PR #8001: I moved them to a separate PR after the discussion there.