mathlib3
7180d2f7 - feat(group_theory/coset): Show that `quotient_group.left_rel` and `left_coset_equivalence` are the same thing (#8382)

Commit

4 years ago

feat(group_theory/coset): Show that `quotient_group.left_rel` and `left_coset_equivalence` are the same thing (#8382) Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Author

eric-wieser

Parents

32c82274

mathlib3 7180d2f7 - feat(group_theory/coset): Show that `quotient_group.left_rel` and `left_coset_equivalence` are the same thing (#8382)

mathlib3
7180d2f7 - feat(group_theory/coset): Show that `quotient_group.left_rel` and `left_coset_equivalence` are the same thing (#8382)