Commit 2023-12-10 09:51 759a69c8

View on Github →

feat: Existence of tranversals of a subgroup (#8932) Specialises the existence of tranversals to the case where one subgroup is contained in another. Also replace ⊤ : Set G by Set.univ and modify the lemma names accordingly. From PFR

Estimated changes

Modified Mathlib/GroupTheory/Complement.lean

added theorem Subgroup.IsComplement.card_mul_card

added theorem Subgroup.IsComplement.mul_eq

modified theorem Subgroup.exists_left_transversal

added theorem Subgroup.exists_left_transversal_of_le

modified theorem Subgroup.exists_right_transversal

added theorem Subgroup.exists_right_transversal_of_le

modified theorem Subgroup.isComplement_singleton_left

modified theorem Subgroup.isComplement_singleton_right

deleted theorem Subgroup.isComplement_singleton_top

added theorem Subgroup.isComplement_singleton_univ

deleted theorem Subgroup.isComplement_top_left

deleted theorem Subgroup.isComplement_top_right

deleted theorem Subgroup.isComplement_top_singleton

added theorem Subgroup.isComplement_univ_left

added theorem Subgroup.isComplement_univ_right

added theorem Subgroup.isComplement_univ_singleton

Modified Mathlib/GroupTheory/HNNExtension.lean

Modified Mathlib/GroupTheory/PushoutI.lean

Modified Mathlib/GroupTheory/Schreier.lean