Structures · Algebra

MulSemiringAction

Typeclass for multiplicative actions by monoids on semirings. This combines DistribMulAction with MulDistribMulAction: it expresses the interplay between the action and both addition and multiplication on the target. Two key axioms are g • (x + y) = (g • x) + (g • y) and g • (x * y) = (g • x) * (g • y). A typical use case is the action of a Galois group $Gal(L/K)$ on the field L.

Defined in

Mathlib.Algebra.Ring.Action.Basic

Shape

2 explicit arguments · adds smul_one, smul_mul