Theorem one_le_zpow_of_nonpos₀

Modification history

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