Theorem one_lt_zpow

Modification history

2024-10-11 15:01

Mathlib/Algebra/Order/Field/Power.lean

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

Modified one_lt_zpow View on Github →

2023-01-02 21:04

Mathlib/Algebra/Order/Field/Power.lean

feat: port algebra.order.field.power (#1256) …

Added one_lt_zpow View on Github →