mathlib3

3d67b696 - chore(algebra/group_power/basic): `pow_abs` does not need commutativity (#7178)