Commit 2023-05-29 08:45 eebd925c

View on Github →

feat: port GroupTheory.Complement (#4349)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Complement.lean

added theorem Subgroup.IsComplement'.card_mul

added theorem Subgroup.IsComplement'.disjoint

added theorem Subgroup.IsComplement'.index_eq_card

added theorem Subgroup.IsComplement'.isCompl

added theorem Subgroup.IsComplement'.sup_eq_top

added theorem Subgroup.IsComplement'.symm

added theorem Subgroup.IsComplement'_bot_left

added theorem Subgroup.IsComplement'_bot_right

added theorem Subgroup.IsComplement'_bot_top

added theorem Subgroup.IsComplement'_comm

added theorem Subgroup.IsComplement'_def

added theorem Subgroup.IsComplement'_iff_card_mul_and_disjoint

added theorem Subgroup.IsComplement'_of_card_mul_and_disjoint

added theorem Subgroup.IsComplement'_of_coprime

added theorem Subgroup.IsComplement'_of_disjoint_and_mul_eq_univ

added theorem Subgroup.IsComplement'_stabilizer

added theorem Subgroup.IsComplement'_top_bot

added theorem Subgroup.IsComplement'_top_left

added theorem Subgroup.IsComplement'_top_right

added theorem Subgroup.IsComplement.card_mul

added theorem Subgroup.IsComplement.existsUnique

added def Subgroup.IsComplement

added theorem Subgroup.IsComplement_iff_existsUnique

added theorem Subgroup.IsComplement_singleton_left

added theorem Subgroup.IsComplement_singleton_right

added theorem Subgroup.IsComplement_singleton_top

added theorem Subgroup.IsComplement_top_left

added theorem Subgroup.IsComplement_top_right

added theorem Subgroup.IsComplement_top_singleton

added theorem Subgroup.MemLeftTransversals.inv_mul_toFun_mem

added theorem Subgroup.MemLeftTransversals.inv_toFun_mul_mem

added theorem Subgroup.MemLeftTransversals.mk''_toEquiv

added theorem Subgroup.MemLeftTransversals.toEquiv_apply

added theorem Subgroup.MemRightTransversals.mk''_toEquiv

added theorem Subgroup.MemRightTransversals.mul_inv_toFun_mem

added theorem Subgroup.MemRightTransversals.toEquiv_apply

added theorem Subgroup.MemRightTransversals.toFun_mul_inv_mem

added theorem Subgroup.card_left_transversal

added theorem Subgroup.card_right_transversal

added theorem Subgroup.coe_transferFunction

added theorem Subgroup.exists_left_transversal

added theorem Subgroup.exists_right_transversal

added def Subgroup.leftTransversals

added theorem Subgroup.mem_leftTransversals_iff_bijective

added theorem Subgroup.mem_leftTransversals_iff_existsUnique_inv_mul_mem

added theorem Subgroup.mem_leftTransversals_iff_existsUnique_quotient_mk''_eq

added theorem Subgroup.mem_rightTransversals_iff_bijective

added theorem Subgroup.mem_rightTransversals_iff_existsUnique_mul_inv_mem

added theorem Subgroup.mem_rightTransversals_iff_existsUnique_quotient_mk''_eq

added theorem Subgroup.mem_transferSet

added theorem Subgroup.quotientEquivSigmaZmod_apply

added theorem Subgroup.quotientEquivSigmaZmod_symm_apply

added theorem Subgroup.range_mem_leftTransversals

added theorem Subgroup.range_mem_rightTransversals

added def Subgroup.rightTransversals

added theorem Subgroup.smul_apply_eq_smul_apply_inv_smul

added theorem Subgroup.smul_toEquiv

added theorem Subgroup.smul_toFun

added theorem Subgroup.transferFunction_apply

added def Subgroup.transferSet

added def Subgroup.transferTransversal

added theorem Subgroup.transferTransversal_apply''

added theorem Subgroup.transferTransversal_apply'

added theorem Subgroup.transferTransversal_apply