Theorems · Inductive type · group theory

MulAction

(α : Type u_9) → Type u_10 → [Monoid α] → Type (max u_10 u_9)

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

Cited by

1,294 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

Monoid