Theorem zpow_pos

Modification history

2024-10-11 15:01

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

chore: generalise `zpow` lemmas from `LinearOrderedSemifield` to `GroupWithZero` (#17539)

Added zpow_pos View on Github →