instSMulCommClass — Mathlib

English

Let R be as above and β be suitable; then SMulCommClass R C_c(α,β) C_c(α,β) holds, i.e., scalar multiplication commutes with multiplication on C_c(α,β): (r f) g = r (f g).

Русский

Пусть R и β удовлетворяют условиям; тогда выполняется SMulCommClass, то есть скаляры и умножение на C_c(α,β) коммутируют: (r f) g = r (f g).

LaTeX

$$$SMulCommClass(R, C_c(α,β), C_c(α,β))$$$

Lean4

instance {R : Type*} [Semiring R] [NonUnitalNonAssocSemiring β] [IsTopologicalSemiring β] [Module R β]
    [ContinuousConstSMul R β] [SMulCommClass R β β] : SMulCommClass R C_c(α, β) C_c(α, β) where
  smul_comm r f
    g := by
    ext
    simp only [smul_eq_mul, coe_smul, coe_mul, Pi.smul_apply, Pi.mul_apply]
    rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]

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