Commit 2021-10-13 15:48 0ce44420
View on Github →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.