instIsCentralScalar — Mathlib

English

If M and α satisfy IsCentralScalar, then M acts centrally on αᵐᵒᵖ, i.e., op_smul_eq_smul holds transported to αᵐᵒᵖ.

Русский

Если есть IsCentralScalar для M и α, то аналогичное свойство верно и для αᵐᵒᵖ: op_smul_eq_smul на αᵐᵒᵖ.

LaTeX

$$$IsCentralScalar\ M\ α \Rightarrow IsCentralScalar\ M\ α^{\mathrm{op}}$ with op_smul_eq_smul preserved.$$

Lean4

@[to_additive]
instance instIsCentralScalar [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] : IsCentralScalar M αᵐᵒᵖ where
  op_smul_eq_smul _ _ := unop_injective <| op_smul_eq_smul _ _

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