Commit 2024-07-26 08:51 24977e64

View on Github →

feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann) (#13047) Lemma of B. H. Neumann on covering a group by finitely many cosets of subgroups.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Finite.lean

added theorem Set.Finite.preimage'

Modified Mathlib/GroupTheory/Complement.lean

added theorem Subgroup.MemLeftTransversals.finite_iff

added theorem Subgroup.MemRightTransversals.finite_iff

Created Mathlib/GroupTheory/CosetCover.lean

added theorem Subgroup.exists_finiteIndex_of_leftCoset_cover

added theorem Subgroup.exists_finiteIndex_of_leftCoset_cover_aux

added theorem Subgroup.exists_index_le_card_of_leftCoset_cover

added theorem Subgroup.exists_leftTransversal_of_FiniteIndex

added theorem Subgroup.finiteIndex_of_leftCoset_cover_const

added theorem Subgroup.index_le_of_leftCoset_cover_const

added theorem Subgroup.leftCoset_cover_const_iff_surjOn

added theorem Subgroup.leftCoset_cover_filter_FiniteIndex

added theorem Subgroup.leftCoset_cover_filter_FiniteIndex_aux

added theorem Subgroup.one_le_sum_inv_index_of_leftCoset_cover

added theorem Subgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq

added theorem Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one

added theorem Submodule.exists_finiteIndex_of_cover

added theorem Subspace.biUnion_ne_univ_of_ne_top

added theorem Subspace.exists_eq_top_of_biUnion_eq_univ

Modified Mathlib/GroupTheory/Index.lean

added theorem Subgroup.finiteIndex_iInf'

added theorem Subgroup.finiteIndex_iInf

Modified docs/references.bib