mathlib

912039d7 - feat(algebra/group_power/lemmas): Positivity of an odd/even power (#9796)

feat(algebra/group_power/lemmas): Positivity of an odd/even power (#9796) This adds `odd.pow_nonneg` and co and `pow_right_comm`. This also deletes `pow_odd_nonneg` and `pow_odd_pos` as they are special cases of `pow_nonneg` and `pow_pos`. To make dot notation work, this renames `(pow/fpow)_(odd/even)_(nonneg/nonpos/pos/neg/abs)` to `(odd/even).(pow/fpow)_(nonneg/nonpos/pos/neg/abs)`