9.3. Notable results
The following are some notable results in Mathlib's group theory library:
-
Lagrange's theorem
Subgroup.card_subgroup_dvd_card -
Sylow's first theorem
Sylow.exists_subgroup_card_pow_prime -
Simplicity of the alternating group
alternatingGroup.isSimpleGroup -
The Schur-Zassenhaus theorem
Subgroup.exists_left_complement'_of_coprime