[Merged by Bors] - feat(GroupTheory/Congruences): add the equiv between congruence relations on a group and its normal subgroup#23269

xroblot wants to merge 14 commits intomasterleanprover-community/mathlib4:masterfrom

xfr-subgroup_orderIsoleanprover-community/mathlib4:xfr-subgroup_orderIsoCopy head branch name to clipboard