Commit 2022-04-25 06:23 6cbf986a

View on Github →

refactor(group_theory/schur_zassenhaus): Golf proof of abelian case (#13622) This PR golfs the proof of the abelian case of Schur-Zassenhaus by switching from a nonstandard definition of the difference of two left transversals to the definition used in transfer.lean.

Estimated changes

Modified src/group_theory/schur_zassenhaus.lean

deleted theorem subgroup.diff_inv

deleted theorem subgroup.diff_mul_diff

deleted theorem subgroup.diff_self

added theorem subgroup.eq_one_of_smul_eq_one

modified theorem subgroup.exists_smul_eq

modified theorem subgroup.is_complement'_stabilizer_of_coprime

modified def subgroup.quotient_diff

added theorem subgroup.smul_diff'

deleted theorem subgroup.smul_diff

added theorem subgroup.smul_diff_smul'

deleted theorem subgroup.smul_diff_smul

deleted theorem subgroup.smul_left_injective