Zulip Chat Archive
Stream: general
Topic: regular action
Kenny Lau (May 30 2020 at 11:21):
/-- The regular action of a monoid on itself by left multiplication. -/
def regular : mul_action α α :=
{ smul := λ a₁ a₂, a₁ * a₂,
one_smul := λ a, one_mul a,
mul_smul := λ a₁ a₂ a₃, mul_assoc _ _ _, }
Kenny Lau (May 30 2020 at 11:21):
why is this one not an instance?
Kenny Lau (May 30 2020 at 11:22):
@Scott Morrison
Kenny Lau (May 30 2020 at 11:22):
oh is it because you might also want conjugation action?
Scott Morrison (May 30 2020 at 11:23):
sounds good :-)
Last updated: Dec 20 2023 at 11:08 UTC