mathlib3

5b7bc676 - refactor(group_theory/subgroup/basic): Make `subgroup.opposite` an `equiv` (#16271)

refactor(group_theory/subgroup/basic): Make `subgroup.opposite` an `equiv` (#16271) There is currently no way to turn a `subgroup Gᵐᵒᵖ` into a `subgroup G`, so this PR bundles `subgroup.opposite` as an `equiv` so that now we can use `subgroup.opposite.symm`.