instIsCentralScalar — Mathlib

English

If β has a central scalar action, then the scalar action on C₀(α,β) is central.

Русский

Если β имеет центральное скалярное действие, то скалярное действие на C₀(α,β) центрально.

LaTeX

$$IsCentralScalar R C₀(α, β) given IsCentralScalar R β and appropriate module structure.$$

Lean4

instance instIsCentralScalar [Zero β] {R : Type*} [Zero R] [SMulWithZero R β] [SMulWithZero Rᵐᵒᵖ β]
    [ContinuousConstSMul R β] [IsCentralScalar R β] : IsCentralScalar R C₀(α, β) :=
  ⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩

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