English
A multiplicative action of a monoid α on a family of monoids f(i) yields a multiplicative action on the Pi-type ∀ i, f(i) defined coordinatewise by (a • x)(i) = a • x(i).
Русский
Действие моноида α на семейство моноидов f(i) порождает произведение действий на Π-тип: (a • x)(i) = a • x(i).
LaTeX
$$$\text{If } \forall i, f(i) \text{ is a Monoid and } \alpha \text{ acts on each } f(i) \text{ by a MulDistribMulAction, then } \alpha \text{ acts on } \forall i, f(i) \text{ by } (a, x)\mapsto (i\mapsto a•x(i)).$$$
Lean4
instance mulDistribMulAction (α) {m : Monoid α} {n : ∀ i, Monoid <| f i} [∀ i, MulDistribMulAction α <| f i] :
@MulDistribMulAction α (∀ i : I, f i) m (@Pi.monoid I f n) :=
{ Pi.mulAction _ with
smul_one := fun _ => funext fun _ => smul_one _
smul_mul := fun _ _ _ => funext fun _ => smul_mul' _ _ _ }
