Theorem zpow_pos

Modification history

2025-04-24 20:04
Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean
chore(Algebra/Order/GroupWithZero): review (#24301) …
Modified zpow_posView on Github →
2025-04-11 08:18
Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean
feat(Order/GroupWithZero): drop more TC assumptions (#23922) …
Modified zpow_posView on Github →
2025-04-10 02:58
Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean
feat(Order/GroupWithZero): drop some `0 ≤ 1` assumptions (#23892) …
Modified zpow_posView on Github →
2024-10-11 15:01
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
chore: generalise `zpow` lemmas from `LinearOrderedSemifield` to `GroupWithZero` (#17539)
Added zpow_posView on Github →