mathlib3
55a7d385 - feat(group_theory/coset): rw lemmas involving quotient_group.mk (#8957)

Commit

4 years ago

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.

Author

tb65536

Parents

baefdf34

mathlib3 55a7d385 - feat(group_theory/coset): rw lemmas involving quotient_group.mk (#8957)

mathlib3
55a7d385 - feat(group_theory/coset): rw lemmas involving quotient_group.mk (#8957)