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.