Theorem zpow_abs_eq_one

Modification history

2024-08-09 11:40

Mathlib/Algebra/Order/Group/Int.lean

chore (Algebra.Order.Group.Int): split file into unbundled and bundled ordered algebra (#15069) …

Modified zpow_abs_eq_one View on Github →

2024-02-15 20:02

Mathlib/Data/Int/Order/Basic.lean

chore: Golf `exists_pow_eq_one_of_zpow_eq_one` (#10559) …

Added zpow_abs_eq_one View on Github →