Structures · Algebra

MulAction

Type class for monoid actions on types, with notation g • p. The MulAction G P typeclass says that the monoid G acts multiplicatively on a type P. More precisely this means that the action satisfies the two axioms 1 • p = p and (g₁ * g₂) • p = g₁ • (g₂ • p). A mathematician might simply say that the monoid G acts on P. For example, if G is a group and X is a type, if a mathematician says say "let G act on the set X" they will probably mean [MulAction G X]. [Wikidata Q288465](https://www.wikidata.org/wiki/Q288465)

Defined in

Mathlib.Algebra.Group.Action.Defs

Shape

2 explicit arguments · adds one_smul