instSMulCommClass — Mathlib

English

If R acts on β and A acts on β, then the two SMuls commute on the function space: smul_comm holds pointwise.

Русский

Если два умножения по скалярам действуют на β, то их действия взаимно commute на пространстве функций; выполняется smul_comm.

LaTeX

$$SMulCommClass R (ZeroAtInftyContinuousMap α β) (ZeroAtInftyContinuousMap α β).$$

Lean4

instance instSMulCommClass {R : Type*} [Semiring R] [NonUnitalNonAssocSemiring β] [IsTopologicalSemiring β] [Module R β]
    [ContinuousConstSMul R β] [SMulCommClass R β β] : SMulCommClass R 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]

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