MulAction versus MonoidAction

Stream: mathlib4

[Xavier Xarles]

It is a bit confusing for me that MulAction is defined for the action of a Monoid, and not for the action of a Semigroup (or just a Multiplicative operation). Something like this...

import Mathlib.Algebra.Group.Commute.Defs


/-- Type class for additive operations actions. -/
class AddAction (G : Type*) (P : Type*) [Add G] extends VAdd G P where
  /-- Associativity of `+` and `+ᵥ` -/
  add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)

/-- Typeclass for multiplicative actions.-/
@[to_additive (attr := ext)]
class MulAction (α : Type*) (β : Type*) [Mul α] extends SMul α β where
  /-- Associativity of `•` and `*` -/
  mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b

/-- Type class for additive monoids actions. -/
class AddMonoidAction (G : Type*) (P : Type*) [AddMonoid G] extends AddAction G P where
  /-- Zero is a neutral element for `+ᵥ` -/
  protected zero_vadd : ∀ p : P, (0 : G) +ᵥ p = p

/-- Typeclass for Monoid actions. This generalizes group actions. -/
@[to_additive (attr := ext)]
class MonoidAction (α : Type*) (β : Type*) [Monoid α] extends MulAction α β where
  /-- One is the neutral element for `•` -/
  protected one_smul : ∀ b : β, (1 : α) • b = b