Theorems · Inductive type · group theory

DistribMulAction

(M : Type u_12) → (A : Type u_13) → [Monoid M] → [AddMonoid A] → Type (max u_12 u_13)

Typeclass for multiplicative actions on additive structures. For example, if G is a group (with group law written as multiplication) and A is an abelian group (with group law written as addition), then to give A a G-module structure (for example, to use the theory of group cohomology) is to say [DistribMulAction G A]. Note in that we do not use the Module typeclass for G-modules, as the Module typeclass is for modules over a ring rather than a group. Mathematically, DistribMulAction G A is equivalent to giving A the structure of a ℤ[G]-module.

Defined in

Mathlib.Algebra.GroupWithZero.Action.Defs

Cited by

584 results in Mathlib

Foundations

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

Assumes

MonoidAddMonoid