lemmas): assume `n ≠ 0` instead of `0 < n` (#17323)

Commit

3 years ago

refactor(algebra/group_power/lemmas): assume `n ≠ 0` instead of `0 < n` (#17323) Also rename `is_unit_pos_pow_iff` to `is_unit_pow_iff`.

Author

urkud

Parents