Commit 2022-03-20 15:25 9502db1f
View on Github →refactor(group_theory/group_action/basic): Golf definition of action on cosets (#12823)
This PR golfs the definition of the left-multiplication action on left cosets.
I deleted mul_left_cosets since it's the same as • and has no API.