mathlib

80d02347 - fix(algebra/group_power): put opposite lemmas in the right namespace (#8100)