Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-05 23:31 a3997288

View on Github →

feat(group_theory/coset): Interaction between quotient_group.mk and right multiplication by elements of the subgroup (#8970) Two helpful lemmas regarding the interaction between quotient_group.mk and right multiplication by elements of the subgroup.

Estimated changes