Structures · Algebra

MulDistribMulAction

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

Shape

2 explicit arguments · adds smul_one, smul_mul