instSMulCommClass — Mathlib

English

Let S and T act on R by scalars and assume their actions commute on R. Then the quadratic algebra QuadraticAlgebra R a b inherits this commuting action, i.e. SMulCommClass S T (QuadraticAlgebra R a b).

Русский

Пусть S и T действуют на R скалярами и их действия взаимно приводят к одному и тому же результату на R. Тогда на квадратичной алгебре QuadraticAlgebra R a b эти действия наследуют это свойство: SMulCommClass S T (QuadraticAlgebra R a b).

LaTeX

$$$SMulCommClass S T (QuadraticAlgebra R a b)$$$

Lean4

instance [SMulCommClass S T R] : SMulCommClass S T (QuadraticAlgebra R a b) where
  smul_comm s t z := by ext <;> exact smul_comm _ _ _

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