Theorem zero_pow_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_pow_eq_one₀View on Github →