instSMulCommClass — Mathlib

English

If SMulCommClass M N α and SMulCommClass M N β hold, then SMulCommClass M N (Sum α β) holds.

Русский

Если существуют SMulCommClass M N α и SMulCommClass M N β, то SMulCommClass M N (Sum α β) выполняется.

LaTeX

$$$[SMulCommClass M N α][SMulCommClass M N β] \Rightarrow SMulCommClass M N (Sum α β).$$$

Lean4

@[to_additive]
instance [SMulCommClass M N α] [SMulCommClass M N β] : SMulCommClass M N (α ⊕ β) :=
  ⟨fun a b x => by
    cases x
    exacts [congr_arg inl (smul_comm _ _ _), congr_arg inr (smul_comm _ _ _)]⟩

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