Theorem zpow_right_strictMono

Modification history

2024-09-24 12:27
Mathlib/Algebra/Order/Group/Basic.lean
chore(Order/Group): golf (#17079) …
Modified zpow_right_strictMonoView on Github →
2024-06-06 18:43
Mathlib/Algebra/Order/Group/Basic.lean
chore: Split `Algebra.GroupPower.Order` (#12964) …
Modified zpow_right_strictMonoView on Github →
2024-01-18 17:23
Mathlib/Algebra/GroupPower/Lemmas.lean
chore: Move order lemmas about `zpow` (#9805) …
Modified zpow_right_strictMonoView on Github →
2023-12-18 07:15
Mathlib/Algebra/GroupPower/Lemmas.lean
chore: Rename pow monotonicity lemmas (#9095) …
Added zpow_right_strictMonoView on Github →