Structures · Algebra
SemigroupAction
Type class for actions by semigroups, with notation g • p.
The SemigroupAction G P typeclass says that the semigroup G acts multiplicatively on a type P.
More precisely this means that the action satisfies the axiom (g₁ * g₂) • p = g₁ • (g₂ • p).
A mathematician might simply say that the semigroup G acts on P.
For example, if G is a semigroup and X is a type, if a mathematician says
say "let G act on the set X" they will probably mean [SemigroupAction G X].
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Shape
- 2 explicit arguments · adds mul_smul
Extends1
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…