Commit 2021-10-16 18:01 5ac586a6

View on Github →

feat(algebra/group_power/order): When a power is less than one (#9700) This proves a bunch of simple order lemmas relating 1, a and a ^ n. I also move pow_le_one upstream as it could already be proved in algebra.group_power.order and remove [nontrivial R] from one_lt_pow.

Estimated changes

Modified src/algebra/group_power/lemmas.lean

added theorem pow_le_of_le_one

deleted theorem pow_le_one

modified theorem pow_le_pow_of_le_one

added theorem sq_le

Modified src/algebra/group_power/order.lean

added theorem one_le_pow_iff_of_nonneg

added theorem one_le_sq_iff

modified theorem one_lt_pow

added theorem one_lt_pow_iff_of_nonneg

added theorem one_lt_sq_iff

added theorem pow_le_one

added theorem pow_le_one_iff_of_nonneg

added theorem pow_lt_one

added theorem pow_lt_one_iff_of_nonneg

added theorem sq_le_one_iff

added theorem sq_lt_one_iff