Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-28 19:44 7180d2f7

View on Github →

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

Estimated changes

Modified src/group_theory/coset.lean

added theorem left_coset_eq_iff

modified def quotient_group.left_rel

added theorem quotient_group.left_rel_r_eq_left_coset_equivalence

modified def quotient_group.quotient

modified def quotient_group.right_rel

added theorem quotient_group.right_rel_r_eq_right_coset_equivalence

added theorem right_coset_eq_iff