mathlib3

ec611821 - feat(algebra/group_power): relate square equality and absolute value equality (#11683)