English
Let α be a Monoid and each f(i) an AddMonoid with a DistribMulAction by α. For i ∈ I, r ∈ α, x ∈ f(i), we have single i (r • x) = r • single i x.
Русский
Пусть α — моноид, и для каждого i множества f(i) является AddMonoid с действием α, распределённым. Тождество: для i, r, x верно single i (r • x) = r • single i x.
LaTeX
$$$\text{For fixed } i,\; (\operatorname{single}_i (r \cdot x)) = r \cdot (\operatorname{single}_i x).$$$
Lean4
theorem single_smul {α} [Monoid α] [∀ i, AddMonoid <| f i] [∀ i, DistribMulAction α <| f i] [DecidableEq I] (i : I)
(r : α) (x : f i) : single i (r • x) = r • single i x :=
single_op (fun i : I => (r • · : f i → f i)) (fun _ => smul_zero _) _ _
