Commit 2023-02-06 07:44 1c7f1a46

View on Github →

feat: port GroupTheory.DoubleCoset (#2076)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/DoubleCoset.lean

added def Doset.Quotient

added theorem Doset.bot_rel_eq_leftRel

added theorem Doset.disjoint_out'

added def Doset.doset

added theorem Doset.doset_eq_of_mem

added theorem Doset.doset_union_leftCoset

added theorem Doset.doset_union_rightCoset

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 theorem Doset.mk_eq_of_doset_eq

added theorem Doset.mk_out'_eq_mul

added theorem Doset.out_eq'

added def Doset.quotToDoset

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_quotToDoset