Commit 2022-04-14 11:12 dd34ffaf

View on Github →

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.

Estimated changes

Modified src/group_theory/schur_zassenhaus.lean

modified theorem subgroup.is_complement'_stabilizer_of_coprime