Theorem zpow_right_strictMono₀

Modification history

2024-10-11 15:01
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
chore: generalise `zpow` lemmas from `LinearOrderedSemifield` to `GroupWithZero` (#17539)
Added zpow_right_strictMono₀View on Github →