Commit 2025-08-03 03:08 0011f417

View on Github →

chore: rename doset to doubleCoset (#27004)

Estimated changes

Modified Mathlib/GroupTheory/DoubleCoset.lean

deleted def Doset.Quotient

deleted theorem Doset.bot_rel_eq_leftRel

deleted theorem Doset.disjoint_out

deleted def Doset.doset

deleted theorem Doset.doset_eq_image2

deleted theorem Doset.doset_eq_of_mem

deleted theorem Doset.doset_union_leftCoset

deleted theorem Doset.doset_union_rightCoset

deleted theorem Doset.eq

deleted theorem Doset.eq_of_not_disjoint

deleted theorem Doset.left_bot_eq_left_quot

deleted theorem Doset.mem_doset

deleted theorem Doset.mem_doset_of_not_disjoint

deleted theorem Doset.mem_doset_self

deleted theorem Doset.mk_eq_of_doset_eq

deleted theorem Doset.mk_out_eq_mul

deleted theorem Doset.out_eq'

deleted def Doset.quotToDoset

deleted theorem Doset.rel_bot_eq_right_group_rel

deleted theorem Doset.rel_iff

deleted theorem Doset.right_bot_eq_right_quot

deleted def Doset.setoid

deleted theorem Doset.union_quotToDoset

added def DoubleCoset.Quotient

added theorem DoubleCoset.bot_rel_eq_leftRel

added theorem DoubleCoset.disjoint_out

added def DoubleCoset.doubleCoset

added theorem DoubleCoset.doubleCoset_eq_image2

added theorem DoubleCoset.doubleCoset_eq_of_mem

added theorem DoubleCoset.doubleCoset_union_leftCoset

added theorem DoubleCoset.doubleCoset_union_rightCoset

added theorem DoubleCoset.eq

added theorem DoubleCoset.eq_of_not_disjoint

added theorem DoubleCoset.left_bot_eq_left_quot

added theorem DoubleCoset.mem_doubleCoset

added theorem DoubleCoset.mem_doubleCoset_of_not_disjoint

added theorem DoubleCoset.mem_doubleCoset_self

added theorem DoubleCoset.mk_eq_of_doubleCoset_eq

added theorem DoubleCoset.mk_out_eq_mul

added theorem DoubleCoset.out_eq'

added def DoubleCoset.quotToDoubleCoset

added theorem DoubleCoset.rel_bot_eq_right_group_rel

added theorem DoubleCoset.rel_iff

added theorem DoubleCoset.right_bot_eq_right_quot

added def DoubleCoset.setoid

added theorem DoubleCoset.union_quotToDoubleCoset