English
If M is a monoid and each fiber α_i has a MulAction of M, then the dependent sum Σ i, α_i carries a MulAction of M by Axiom: m • ⟨i,a⟩ = ⟨i, m • a⟩; the action respects identity and composition.
Русский
Если моноид M действует на каждом α_i, то зависимая сумма Σ i, α_i имеет действие M, заданное m • ⟨i,a⟩ = ⟨i, m • a⟩; тождество и композиция сохраняются.
LaTeX
$$$[\forall i, MulAction M (α_i)] \Rightarrow MulAction M (\Sigma i, α_i),\; (m,⟨i,a⟩) \mapsto ⟨i, m·a⟩.$$$
Lean4
@[to_additive]
instance {m : Monoid M} [∀ i, MulAction M (α i)] : MulAction M (Σ i, α i)
where
mul_smul a b
x := by
cases x
rw [smul_mk, smul_mk, smul_mk, mul_smul]
one_smul
x := by
cases x
rw [smul_mk, one_smul]
