Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-10 07:37 0fd99294

View on Github →

feat(group_theory/double_cosets): definition of double cosets and some basic lemmas. (#9490) This contains the definition of double cosets and some basic lemmas about them, such as "the whole group is the disjoint union of its double cosets" and relationship to usual group quotients.

Estimated changes

Created src/group_theory/double_coset.lean

added theorem doset.bot_rel_eq_left_rel

added theorem doset.disjoint_out'

added theorem doset.doset_eq_of_mem

added theorem doset.doset_union_left_coset

added theorem doset.doset_union_right_coset

added theorem doset.eq

added theorem doset.eq_of_not_disjoint

added theorem doset.left_bot_eq_left_quot

added theorem doset.mem_doset

added theorem doset.mem_doset_of_not_disjoint

added theorem doset.mem_doset_self

added def doset.mk

added theorem doset.mk_eq_of_doset_eq

added theorem doset.mk_out'_eq_mul

added theorem doset.out_eq'

added def doset.quot_to_doset

added def doset.quotient

added theorem doset.rel_bot_eq_right_group_rel

added theorem doset.rel_iff

added theorem doset.right_bot_eq_right_quot

added def doset.setoid

added theorem doset.union_quot_to_doset

added def doset

Modified src/group_theory/subgroup/pointwise.lean

added theorem subgroup.singleton_mul_subgroup

added theorem subgroup.subgroup_mul_singleton