Commit 2026-03-20 16:11 7194d2f6

View on Github →

feat(GroupTheory/DoubleCoset): multiple lemmas (#27229) From FLT

Estimated changes

Modified Mathlib/GroupTheory/DoubleCoset.lean

modified theorem DoubleCoset.bot_rel_eq_leftRel

modified theorem DoubleCoset.disjoint_out

modified theorem DoubleCoset.doubleCoset_eq_of_mem

modified theorem DoubleCoset.doubleCoset_union_leftCoset

modified theorem DoubleCoset.doubleCoset_union_rightCoset

added theorem DoubleCoset.eq''

modified theorem DoubleCoset.eq

modified theorem DoubleCoset.eq_of_not_disjoint

added theorem DoubleCoset.finite_quotient_iff_exists_finset_iUnion_eq_univ

added theorem DoubleCoset.iUnion_finset_leftRel_eq_univ_of_leftRel

added theorem DoubleCoset.iUnion_finset_rightRel_eq_univ_of_rightRel

added theorem DoubleCoset.iUnion_image_mk_leftRel

added theorem DoubleCoset.iUnion_image_mk_rightRel

added theorem DoubleCoset.iUnion_quotToDoubleCoset

modified theorem DoubleCoset.left_bot_eq_left_quot

modified theorem DoubleCoset.mem_doubleCoset

modified theorem DoubleCoset.mem_doubleCoset_of_not_disjoint

modified theorem DoubleCoset.mem_doubleCoset_self

added theorem DoubleCoset.mem_quotToDoubleCoset_iff

modified theorem DoubleCoset.mk_eq_of_doubleCoset_eq

modified theorem DoubleCoset.mk_out_eq_mul

modified theorem DoubleCoset.out_eq'

modified theorem DoubleCoset.rel_bot_eq_right_group_rel

modified theorem DoubleCoset.rel_iff

modified theorem DoubleCoset.right_bot_eq_right_quot

deleted theorem DoubleCoset.union_quotToDoubleCoset