English
There is a natural action of the product monoid ∀i αi on the product ∀i βi, given by m • x = (i ↦ m(i) • x(i)).
Русский
Существует естественное действие на произведении ∀i βi от произведения монойдов ∀ i αi, задаваемое покоординатно: (m • x)(i) = m(i) • x(i).
LaTeX
$$$\text{MulAction }\big(\forall i, \alpha_i\big)\big(\forall i, \beta_i\big)\text{ by } (m\cdot x)(i)=m(i)\cdot x(i).$$$
Lean4
@[to_additive]
instance mulAction' {m : ∀ i, Monoid (α i)} [∀ i, MulAction (α i) (β i)] :
@MulAction (∀ i, α i) (∀ i, β i) (@Pi.monoid ι α m)
where
smul := (· • ·)
mul_smul _ _ _ := funext fun _ ↦ mul_smul _ _ _
one_smul _ := funext fun _ ↦ one_smul _ _
