English
Let ι be an index type, for each i a type α i, and for each i a family δ i j with a γ-action; the collection Π₀ (i : ι) (j : α i), δ i j carries a natural γ-action defined componentwise, making it a DistribMulAction.
Русский
Пусть ι — множество индексов, для каждого i есть тип α i, и для каждого i и j имеется семейство δ i j с действием моноида γ; совокупность Π₀ (i : ι) (j : α i), δ i j естественным образом наследует действие γ, определяемое по компонентам, образуя распределимое действие.
LaTeX
$$$$ \\operatorname{DistribMulAction}\\left(\\gamma,\\; \\Pi_0 (i:\\iota)(j:\\alpha i),\\; \\delta(i,j)\\right) $$$$
Lean4
instance distribMulAction₂ [Monoid γ] [∀ i j, AddMonoid (δ i j)] [∀ i j, DistribMulAction γ (δ i j)] :
DistribMulAction γ (Π₀ (i : ι) (j : α i), δ i j) :=
@DFinsupp.distribMulAction ι _ (fun i => Π₀ j, δ i j) _ _ _
