Commit 2021-11-23 16:49 7a6e6d8b

View on Github →

feat(group_theory/schur_zassenhaus): Prove the full Schur-Zassenhaus theorem (#10283) Previously, the Schur-Zassenhaus theorem was only proved for abelian normal subgroups. This PR removes the abelian assumption.

Estimated changes

Modified src/group_theory/schur_zassenhaus.lean

modified theorem subgroup.exists_left_complement'_of_coprime

added theorem subgroup.exists_left_complement'_of_coprime_of_fintype

modified theorem subgroup.exists_right_complement'_of_coprime

added theorem subgroup.exists_right_complement'_of_coprime_of_fintype

added theorem subgroup.schur_zassenhaus_induction.step7