Commit 2025-01-03 11:02 ef4bb8a4

View on Github →

chore: turn left and right transversals from sets to types (#20041) The sets both duplicate Subgroup.IsComplement.

Estimated changes

Modified Mathlib/GroupTheory/Complement.lean

added theorem Subgroup.IsComplement.card_left

added theorem Subgroup.IsComplement.card_right

added theorem Subgroup.IsComplement.finite_left_iff

added theorem Subgroup.IsComplement.finite_right_iff

added theorem Subgroup.IsComplement.inv_mul_toLeftFun_mem

added theorem Subgroup.IsComplement.inv_toLeftFun_mul_mem

added theorem Subgroup.IsComplement.leftQuotientEquiv_apply

added theorem Subgroup.IsComplement.mk''_rightQuotientEquiv

added theorem Subgroup.IsComplement.mul_inv_toRightFun_mem

added theorem Subgroup.IsComplement.quotientGroupMk_leftQuotientEquiv

added theorem Subgroup.IsComplement.rightQuotientEquiv_apply

added theorem Subgroup.IsComplement.toRightFun_mul_inv_mem

deleted theorem Subgroup.MemLeftTransversals.finite_iff

deleted theorem Subgroup.MemLeftTransversals.inv_mul_toFun_mem

deleted theorem Subgroup.MemLeftTransversals.inv_toFun_mul_mem

deleted theorem Subgroup.MemLeftTransversals.mk''_toEquiv

deleted theorem Subgroup.MemLeftTransversals.toEquiv_apply

deleted theorem Subgroup.MemRightTransversals.finite_iff

deleted theorem Subgroup.MemRightTransversals.mk''_toEquiv

deleted theorem Subgroup.MemRightTransversals.mul_inv_toFun_mem

deleted theorem Subgroup.MemRightTransversals.toEquiv_apply

deleted theorem Subgroup.MemRightTransversals.toFun_mul_inv_mem

added theorem Subgroup.exists_isComplement_left

added theorem Subgroup.exists_isComplement_right

added theorem Subgroup.isComplement_iff_existsUnique_inv_mul_mem

added theorem Subgroup.isComplement_iff_existsUnique_mul_inv_mem

added theorem Subgroup.isComplement_range_left

added theorem Subgroup.isComplement_range_right

added theorem Subgroup.isComplement_subgroup_left_iff_bijective

added theorem Subgroup.isComplement_subgroup_left_iff_existsUnique_quotientMk''

added theorem Subgroup.isComplement_subgroup_right_iff_bijective

added theorem Subgroup.isComplement_subgroup_right_iff_existsUnique_quotientGroupMk

modified theorem Subgroup.smul_apply_eq_smul_apply_inv_smul

added theorem Subgroup.smul_leftQuotientEquiv

deleted theorem Subgroup.smul_toEquiv

deleted theorem Subgroup.smul_toFun

added theorem Subgroup.smul_toLeftFun

Modified Mathlib/GroupTheory/CosetCover.lean

Modified Mathlib/GroupTheory/HNNExtension.lean

Modified Mathlib/GroupTheory/PushoutI.lean

Modified Mathlib/GroupTheory/Schreier.lean

modified theorem Subgroup.closure_mul_image_eq

modified theorem Subgroup.closure_mul_image_eq_top

Modified Mathlib/GroupTheory/SchurZassenhaus.lean

Modified Mathlib/GroupTheory/Transfer.lean

modified def Subgroup.transferTransversal