Commit 2021-07-24 15:30 8a0d5e07

View on Github →

feat(group_theory/complement): define subgroup complement, prove Schur-Zassenhaus (#8008) Defines complements, and proves Schur-Zassenhaus for abelian normal subgroups.

Estimated changes

Created src/group_theory/complement.lean

added theorem subgroup.diff_inv

added theorem subgroup.diff_mul_diff

added theorem subgroup.diff_self

added theorem subgroup.exists_left_complement_of_coprime

added theorem subgroup.exists_right_complement_of_coprime

added theorem subgroup.exists_smul_eq

added theorem subgroup.is_complement.exists_unique

added theorem subgroup.is_complement.symm

added def subgroup.is_complement

added theorem subgroup.is_complement_comm

added theorem subgroup.is_complement_iff_exists_unique

added theorem subgroup.is_complement_of_coprime

added theorem subgroup.is_complement_of_disjoint

added theorem subgroup.is_complement_stabilizer_of_coprime

added def subgroup.left_transversals

added theorem subgroup.mem_left_transversals_iff_bijective

added theorem subgroup.mem_left_transversals_iff_exists_unique_inv_mul_mem

added theorem subgroup.mem_left_transversals_iff_exists_unique_quotient_mk'_eq

added theorem subgroup.mem_right_transversals_iff_bijective

added theorem subgroup.mem_right_transversals_iff_exists_unique_mul_inv_mem

added theorem subgroup.mem_right_transversals_iff_exists_unique_quotient_mk'_eq

added def subgroup.quotient_diff

added def subgroup.right_transversals

added theorem subgroup.smul_diff

added theorem subgroup.smul_diff_smul

added theorem subgroup.smul_injective

added theorem subgroup.smul_symm_apply_eq_mul_symm_apply_inv_smul

Modified src/group_theory/order_of_element.lean

added theorem inf_eq_bot_of_coprime

Modified src/group_theory/subgroup.lean

added structure add_subgroup.is_commutative

added structure subgroup.is_commutative