instSMulCommClass — Mathlib

English

If M,N are represented with SMul on α, αᵐᵒᵖ inherits SMulCommClass M N αᵐᵒᵖ from SMulCommClass M N α via unop.

Русский

Если имеются действия SMul на α со стороны M и N, то на αᵐᵒᵖ действует SMulCommClass M N αᵐᵒᵖ выводом через unop.

LaTeX

$$$\text{If } [SMul M α], [SMul N α], [SMulCommClass M N α],\;\text{then } SMulCommClass M N α^{\mathrm{op}}$$$

Lean4

@[to_additive]
instance instSMulCommClass [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass M N αᵐᵒᵖ where
  smul_comm _ _ _ := unop_injective <| smul_comm _ _ _

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