Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-21 20:06 912039d7

View on Github →

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)

Estimated changes

deleted theorem abs_fpow_even
added theorem even.abs_fpow
added theorem even.fpow_abs
added theorem even.fpow_neg
added theorem even.fpow_nonneg
added theorem even.fpow_pos
modified theorem fpow_bit0_abs
deleted theorem fpow_even_abs
deleted theorem fpow_even_neg
deleted theorem fpow_even_nonneg
deleted theorem fpow_even_pos
deleted theorem fpow_odd_neg
deleted theorem fpow_odd_nonneg
deleted theorem fpow_odd_nonpos
deleted theorem fpow_odd_pos
added theorem odd.fpow_neg
added theorem odd.fpow_nonneg
added theorem odd.fpow_nonpos
added theorem odd.fpow_pos
added theorem pow_right_comm
added theorem even.pow_abs
added theorem even.pow_nonneg
added theorem even.pow_pos
added theorem even.pow_pos_iff
added theorem odd.pow_neg
added theorem odd.pow_neg_iff
added theorem odd.pow_nonneg_iff
added theorem odd.pow_nonpos
added theorem odd.pow_nonpos_iff
added theorem odd.pow_pos_iff
modified theorem pow_bit0_abs
deleted theorem pow_even_abs
deleted theorem pow_even_nonneg
deleted theorem pow_even_pos
deleted theorem pow_odd_neg
deleted theorem pow_odd_nonneg
deleted theorem pow_odd_nonpos
deleted theorem pow_odd_pos