mathlib

0bc09d9a - feat(algebra/ordered_field): a few monotonicity results for powers (#8022)

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.