smulCommClass — Mathlib

English

If VAdd α γ, VAdd β γ and VAddCommClass α β γ, then SMulCommClass (Multiplicative α) (Multiplicative β) γ holds, i.e., Units preserve commutativity of actions on γ.

Русский

Если VAddα γ, VAddβ γ и VAddCommClass α β γ, то SMulCommClass (Multiplicative α) (Multiplicative β) γ: действия единиц сохраняют коммутативность.

LaTeX

$$$ SMulCommClass (Multiplicative \\alpha) (Multiplicative \\beta) \\gamma $$$

Lean4

instance smulCommClass [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
    SMulCommClass (Multiplicative α) (Multiplicative β) γ :=
  ⟨@vadd_comm α β _ _ _ _⟩

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