Commit 2021-11-04 07:56 8658f40c

View on Github →

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.

Estimated changes

Modified src/algebra/group_power/lemmas.lean

added theorem odd.strict_mono_pow

modified theorem one_add_mul_le_pow'

modified theorem pow_le_of_le_one

modified theorem pow_le_pow_of_le_one

modified theorem pow_lt_pow_iff_of_lt_one

modified theorem pow_lt_pow_of_lt_one

modified theorem sq_le

Modified src/algebra/group_power/order.lean

modified theorem one_le_pow_of_one_le

modified theorem one_lt_pow

modified theorem pow_add_pow_le

added theorem pow_bit0_pos_of_neg

added theorem pow_bit1_neg

modified theorem pow_le_one

modified theorem pow_le_pow

modified theorem pow_lt_one

modified theorem pow_lt_pow

modified theorem pow_lt_pow_iff

modified theorem pow_lt_pow_of_lt_left

modified theorem pow_mono

modified theorem pow_nonneg

modified theorem pow_pos

added theorem sq_pos_of_neg

added theorem sq_pos_of_pos

modified theorem strict_mono_on_pow

modified theorem strict_mono_pow