Theorem abs_pow_eq_one

Modification history

2024-01-18 17:23
Mathlib/Algebra/GroupPower/Order.lean
chore: Move order lemmas about `zpow` (#9805) …
Modified abs_pow_eq_oneView on Github →
2023-12-18 07:15
Mathlib/Algebra/GroupPower/Order.lean
chore: Rename pow monotonicity lemmas (#9095) …
Modified abs_pow_eq_oneView on Github →
2023-05-07 09:18
Mathlib/Algebra/GroupPower/Order.lean
chore: forward port leanprover-community/mathlib#18866 (#3813)
Added abs_pow_eq_oneView on Github →