instSMulCommClass — Mathlib

English

If each fiber α_i carries commuting M- and N-actions (SMulCommClass M N (α_i)) for all i, then the Σ-type (sum over i) also carries a SMulCommClass M N (Σ i, α_i).

Русский

Если для каждой Fiber α_i заданы взаимно коммутируемые действия M и N (SMulCommClass M N (α_i)), то Σ-тип (сумма) также имеет SMulCommClass M N (Σ i, α_i).

LaTeX

$$$[\forall i, SMulCommClass M N (α_i)] \Rightarrow [SMulCommClass M N (\Sigma i, α_i)].$$$

Lean4

@[to_additive]
instance [∀ i, SMulCommClass M N (α i)] : SMulCommClass M N (Σ i, α i) :=
  ⟨fun a b x => by
    cases x
    rw [smul_mk, smul_mk, smul_mk, smul_mk, smul_comm]⟩

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