smulCommClass — Mathlib

English

There is a commutation structure between two scalar actions on normed add group homs, forming a SMulCommClass.

Русский

Существует структура взаимного коммутирования двух действий скаляров на гомоморфизма NormedAddGroupHom, образующая SMulCommClass.

LaTeX

$$$$ [SMulCommClass\ R\ R'\ (NormedAddGroupHom\ V_1\ V_2)] $$$$

Lean4

instance smulCommClass [SMulCommClass R R' V₂] : SMulCommClass R R' (NormedAddGroupHom V₁ V₂) where
  smul_comm _ _ _ := ext fun _ => smul_comm _ _ _

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