Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-02 14:43 ff05d3af

View on Github →

feat(algebra/group_power/lemmas): sign of even/odd powers (#5990) Added theorems about the sign of even and odd natural powers.

Estimated changes

modified theorem one_add_mul_le_pow
modified theorem one_add_mul_sub_le_pow
modified theorem pow_bit1_neg_iff
modified theorem pow_bit1_nonneg_iff
modified theorem pow_bit1_nonpos_iff
modified theorem pow_bit1_pos_iff
added theorem pow_even_nonneg
added theorem pow_even_pos
added theorem pow_odd_neg
added theorem pow_odd_nonneg
added theorem pow_odd_nonpos
added theorem pow_odd_pos