mathlib3

ffd1e5cb - feat(group_theory/quotient_group): congr for lifting an isomorphism to group quotients (#16726)

feat(group_theory/quotient_group): congr for lifting an isomorphism to group quotients (#16726) If `G` and `H` are isomorphic, and the isomorphism maps the subgroup `G'` to `H'`, then the quotients `G ⧸ G'` and `H ⧸ H'` are also isomorphic. Useful for showing the class group doesn't depend on a choice of field of fractions.