mathlib3

6cbf986a - refactor(group_theory/schur_zassenhaus): Golf proof of abelian case (#13622)

refactor(group_theory/schur_zassenhaus): Golf proof of abelian case (#13622) This PR golfs the proof of the abelian case of Schur-Zassenhaus by switching from a nonstandard definition of the difference of two left transversals to the definition used in `transfer.lean`.