Commit 2022-08-31 17:11 5b7bc676
View on Github →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.