mathlib3

63e75351 - chore(group_theory/coset): right_coset additions and module doc (#6371)

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. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>