A multiplicative action on a monoid is distributive over its self-action

A multiplicative distributive action of G on a monoid A, such as a MulSemiringAction, has g • (a * b) = g • a * g • b. Read with A acting on itself by left multiplication, this is SMulDistribClass G A A, the form taken by statements about semilinear actions on A-modules when the module is A itself.

Main results

• TauCeti.smulDistribClass_self: SMulDistribClass G A A for a MulDistribMulAction G A.

instance TauCeti.smulDistribClass_self (G : Type u_1) (A : Type u_2) [Monoid G] [Monoid A] [MulDistribMulAction G A] : SMulDistribClass G A A

A multiplicative distributive action of G on a monoid A distributes over the action of A on itself by left multiplication.