Theorem zero_zpow_eq_one₀

Modification history

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