Zulip Chat Archive

Stream: general

Topic: regular action


view this post on Zulip Kenny Lau (May 30 2020 at 11:21):

https://github.com/leanprover-community/mathlib/blob/62cb7f2f34079df7c054239d467f72c61be4f63a/src/group_theory/group_action.lean#L74-L78

/-- 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 _ _ _, }

view this post on Zulip Kenny Lau (May 30 2020 at 11:21):

why is this one not an instance?

view this post on Zulip Kenny Lau (May 30 2020 at 11:22):

@Scott Morrison

view this post on Zulip Kenny Lau (May 30 2020 at 11:22):

oh is it because you might also want conjugation action?

view this post on Zulip Scott Morrison (May 30 2020 at 11:23):

sounds good :-)


Last updated: May 10 2021 at 19:16 UTC