Zulip Chat Archive

Stream: Is there code for X?

Topic: mul_action on quotient_group.quotient


view this post on Zulip 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?

view this post on Zulip Eric Wieser (Dec 12 2020 at 12:58):

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

view this post on Zulip 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)

view this post on Zulip 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