English
If M, N act on α with SMul and SMulCommClass M N α, then the coordinatewise action on the Pi-type ι → α is SMulCommClass M N (ι → α).
Русский
Если на α действует пара скаляров M, N с комм-совместимостью, то на функции из индексов в α действует та же коммутативность по координатам: SMulCommClass M N (ι → α).
LaTeX
$$$SMulCommClass\ M\ N\ (\iota \to \alpha).$$$
Lean4
/-- Non-dependent version of `Pi.smulCommClass`. Lean gets confused by the dependent instance if
this is not present. -/
@[to_additive /-- Non-dependent version of `Pi.vaddCommClass`. Lean gets confused by the dependent
instance if this is not present. -/
]
instance smulCommClass {α : Type*} [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass M N (ι → α) :=
Pi.smulCommClass
