Theorem zpow_le_zpow_right₀

Modification history

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