Theorem zpow_eq_one_iff_right₀

Modification history

2024-10-21 14:11
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
feat: `a ^ n = 1 ↔ n = 0` and similar (#17745) …
Added zpow_eq_one_iff_right₀View on Github →