mul_action on quotient_group.quotient

Stream: Is there code for X?

[Eric Wieser]

Is there a mul_action instance on docs#quotient_group.quotient that corresponds to left-multiplication under the quotient?

[Eric Wieser]

With smul := fun r, quotient.map' (λ x, r * x) sorry, where I have a proof of the sorry locally

[Eric Wieser]

(note that in the case I'm thinking of, the subgroup I'm taking the quotient by is not normal)

[Eric Wieser]

docs#mul_action.quotient, I was distracted looking in quotient_group