smulCommClass — Mathlib

English

If each α i is acted on by M and N and SMulCommClass M N (α i) holds for all i, then SMulCommClass M N (∀ i, α i).

Русский

Если для каждого i имеется действие M и N на α_i и SMulCommClass M N (α_i) выполняется для всех i, то SMulCommClass M N (∀ i, α_i).

LaTeX

$$$\text{SMulCommClass } M N (∀ i, α i)$ given $[\forall i, SMul M (α i)] [\forall i, SMul N (α i)] [\forall i, SMulCommClass M N (α i)]$$$

Lean4

@[to_additive]
instance smulCommClass [∀ i, SMul M (α i)] [∀ i, SMul N (α i)] [∀ i, SMulCommClass M N (α i)] :
    SMulCommClass M N (∀ i, α i) where smul_comm x y z := funext fun i ↦ smul_comm x y (z i)

Похожие утверждения