instIsCentralScalar — Mathlib

English

If β has Zero and IsCentralScalar properties, then C_c(α,β) inherits IsCentralScalar: scalars commute with functions pointwise.

Русский

Если β имеет ноль и IsCentralScalar, то C_c(α,β) наследует IsCentralScalar: скаляры коммутируют с функциями по точкам.

LaTeX

$$$$ \text{IsCentralScalar}(R, C_c(α,β)) $$$$

Lean4

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

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