Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quotient_group.left_rel_r_eq_left_coset_equivalence

Modification history

2021-07-28 19:44

src/group_theory/coset.lean

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

Added quotient_group.left_rel_r_eq_left_coset_equivalence View on Github →