lemmas): remove commutativity requirement from `is_unit_pos_pow_iff`

Commit

4 years ago

feat(algebra/group_power/lemmas): remove commutativity requirement from `is_unit_pos_pow_iff` Also adds a simp lemma, is_unit_pow_succ_iff

Author

eric-wieser

Parents