English
If M is a monoid and each fiber α_i has a MulAction M, then the Sigma-type Σ i α_i has a MulAction M given by m · ⟨i, a⟩ = ⟨i, m · a⟩; the action axioms follow from those on the fibers.
Русский
Если моноид M, и на каждом α_i задано действие M, то Σ i α_i имеет действие M: m · ⟨i, a⟩ = ⟨i, m · a⟩.
LaTeX
$$$[\forall i, MulAction M (α_i)] \Rightarrow MulAction M (\Sigma i, α_i),\; m \cdot ⟨i,a⟩ = ⟨i,m\cdot a⟩.$$$
Lean4
@[to_additive]
instance {m : Monoid M} [MulAction M α] [MulAction M β] : MulAction M (α ⊕ β)
where
mul_smul a b
x := by
cases x
exacts [congr_arg inl (mul_smul _ _ _), congr_arg inr (mul_smul _ _ _)]
one_smul
x := by
cases x
exacts [congr_arg inl (one_smul _ _), congr_arg inr (one_smul _ _)]
