Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-13 03:30 dd4c2044

View on Github →

feat(algebra/group_power/order): add monotonicity lemmas (#17895) The existing strict_mono_pow lemma is renamed to pow_strict_mono_right to match the new pow_strict_mono_right'. From this zulip thread.

Estimated changes

added theorem le_max_of_sq_le_mul
added theorem le_of_pow_le_pow'
added theorem lt_max_of_sq_lt_mul
added theorem lt_of_pow_lt_pow'
added theorem min_le_of_mul_le_sq
added theorem min_lt_of_mul_lt_sq
added theorem monotone.pow_right
added theorem pow_mono_right
added theorem pow_strict_mono_right'
added theorem pow_strict_mono_right
added theorem strict_mono.pow_right'
deleted theorem strict_mono_pow