Mathlib v3 is deprecated. Go to Mathlib v4

Theorem left_coset_eq_iff

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 left_coset_eq_iff View on Github →