instIsCentralScalar — Mathlib

English

If R acts centrally on M and there are continuous scalar multiplications, then R acts centrally on C(α, M).

Русский

Если скаляры R действуют централизованно на M и есть непрерывное скалярное умножение, то R действует централизованно на C(α, M).

LaTeX

$$$ IsCentralScalar R C(\alpha, M). $$$

Lean4

instance [SMul R M] [SMul Rᵐᵒᵖ M] [ContinuousConstSMul R M] [IsCentralScalar R M] : IsCentralScalar R C(α, M) where
  op_smul_eq_smul _ _ := ext fun _ => op_smul_eq_smul _ _

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