mathlib

9502db1f - refactor(group_theory/group_action/basic): Golf definition of action on cosets (#12823)

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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>