## Stream: general

### Topic: regular action

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


#### Kenny Lau (May 30 2020 at 11:21):

why is this one not an instance?

@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: May 10 2021 at 19:16 UTC