Theorems · Inductive type · group theory

MulDistribMulAction

(M : Type u_9) → (N : Type u_10) → [Monoid M] → [Monoid N] → Type (max u_10 u_9)

Typeclass for multiplicative actions on multiplicative structures. The key axiom here is smul_mul : g • (x * y) = (g • x) * (g • y). If G is a multiplicative group with automorphism group Γ, then there is a natural instance of MulDistribMulAction Γ G. The axiom is also satisfied by a Galois group $Gal(L/K)$ acting on the field L, but here you can use the even stronger class MulSemiringAction, which captures how the action plays with both multiplication and addition.

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

120 results in Mathlib

Foundations

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

Assumes

MonoidMonoid