mathlib

dd34ffaf - refactor(group_theory/schur_zassenhaus): Golf using `is_complement'_stabilizer` (#13392)

refactor(group_theory/schur_zassenhaus): Golf using `is_complement'_stabilizer` (#13392) This PR golfs the proof of the abelian case of Schur-Zassenhaus using the new lemma `is_complement'_stabilizer`.