instIsCentralScalar — Mathlib

English

There is a central scalar action on the Double Centralizer algebra: for any r in R and a in 𝓜(𝕜, A), r acts centrally, i.e., r·a = a·r.

Русский

Существует центральное действие скаляра на двецентрическую алгебру: для любого r в R и a в 𝓜(𝕜, A) выполняется r·a = a·r.

LaTeX

$$$IsCentralScalar\, R\, (𝓜(𝕜, A))$$$

Lean4

instance instIsCentralScalar {R : Type*} [Semiring R] [Module R A] [SMulCommClass 𝕜 R A] [ContinuousConstSMul R A]
    [IsScalarTower R A A] [SMulCommClass R A A] [Module Rᵐᵒᵖ A] [IsCentralScalar R A] : IsCentralScalar R 𝓜(𝕜, A) where
  op_smul_eq_smul _ a := ext (𝕜 := 𝕜) (A := A) _ _ <| op_smul_eq_smul _ a.toProd

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