Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-02 12:25 55a7d385

View on Github →

feat(group_theory/coset): rw lemmas involving quotient_group.mk (#8957) When doing computations with quotient groups, I found these lemmas to be helpful when rewriting.

Estimated changes