Commit 2023-06-07 15:05 050bf14d

View on Github →

feat: port GroupTheory.SchurZassenhaus (#4752)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/SchurZassenhaus.lean

added def Subgroup.QuotientDiff

added theorem Subgroup.SchurZassenhausInduction.step7

added theorem Subgroup.eq_one_of_smul_eq_one

added theorem Subgroup.exists_left_complement'_of_coprime

added theorem Subgroup.exists_left_complement'_of_coprime_of_fintype

added theorem Subgroup.exists_right_complement'_of_coprime

added theorem Subgroup.exists_right_complement'_of_coprime_of_fintype

added theorem Subgroup.exists_smul_eq

added theorem Subgroup.isComplement'_stabilizer_of_coprime

added theorem Subgroup.smul_diff'

added theorem Subgroup.smul_diff_smul'