even power without linearity (#10122)

Commit

4 years ago

feat(algebra/group_power/order): Sign of an odd/even power without linearity (#10122) This proves that `a < 0 → 0 < a ^ bit0 n` and `a < 0 → a ^ bit1 n < 0` in an `ordered_semiring`.

Author

YaelDillies

Parents

4770a6a7

mathlib3 8658f40c - feat(algebra/group_power/order): Sign of an odd/even power without linearity (#10122)

mathlib3
8658f40c - feat(algebra/group_power/order): Sign of an odd/even power without linearity (#10122)