Commit 2021-02-23 21:11 63e75351

View on Github →

chore(group_theory/coset): right_coset additions and module doc (#6371) This PR dualises two results from left_coset to right_coset and adds a module doc.

Estimated changes

Modified src/group_theory/coset.lean

deleted def left_coset_equiv

deleted theorem left_coset_equiv_rel

added def left_coset_equivalence

added theorem left_coset_equivalence_rel

added def quotient_group.right_rel

added def right_coset_equivalence

added theorem right_coset_equivalence_rel

added def subgroup.right_coset_equiv_subgroup