Stream: Is there code for X?
Eric Wieser (Dec 12 2020 at 12:57):
Is there a
mul_action instance on docs#quotient_group.quotient that corresponds to left-multiplication under the quotient?
Eric Wieser (Dec 12 2020 at 12:58):
smul := fun r, quotient.map' (λ x, r * x) sorry, where I have a proof of the
Eric Wieser (Dec 12 2020 at 13:00):
(note that in the case I'm thinking of, the subgroup I'm taking the quotient by is not normal)
Eric Wieser (Dec 12 2020 at 13:23):
docs#mul_action.quotient, I was distracted looking in quotient_group
Last updated: May 16 2021 at 05:21 UTC