mathlib

0ce44420 - refactor(algebra/group_power/order): relax linearity condition on `one_lt_pow` (#9696)

refactor(algebra/group_power/order): relax linearity condition on `one_lt_pow` (#9696) `[linear_ordered_semiring R]` becomes `[ordered_semiring R] [nontrivial R]`. I also golf the proof and move ìt from `algebra.field_power` to `algebra.group_power.order`, where it belongs.