Theorem pow_right_mono

Modification history

2024-10-07 17:59

Mathlib/Algebra/Order/Ring/Basic.lean

chore: generalise lemmas from `OrderedSemiring` to `MonoidWithZero` (#17412) …

Deleted pow_right_mono View on Github →

2023-12-18 07:15

Mathlib/Algebra/GroupPower/Order.lean

chore: Rename pow monotonicity lemmas (#9095) …

Added pow_right_mono View on Github →