vaddCommClass — Mathlib

English

If SMul α γ, SMul β γ and SMulCommClass α β γ hold, then VAddCommClass (Additive α) (Additive β) γ holds; the additive versions still commute on γ.

Русский

Если выполняются SMul α γ, SMul β γ и SMulCommClass α β γ, то VAddCommClass (Additive α) (Additive β) γ сохраняется; действия суммирования в дополнение сохраняют коммутативность на γ.

LaTeX

$$$ SMul \\alpha \\gamma \\;\\; SMul \\beta \\gamma \\;\\; SMulCommClass \\alpha \\beta \\gamma \\Rightarrow VAddCommClass (Additive \\alpha) (Additive \\beta) \\gamma $$$

Lean4

instance vaddCommClass [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : VAddCommClass (Additive α) (Additive β) γ :=
  ⟨@smul_comm α β _ _ _ _⟩

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