instSMul — Mathlib

English

CentroidHom α is compatible with commuting scalars from M and N: for any SMulCommClass M N α, CentroidHom α inherits SMulCommClass M N.

Русский

CentroidHom α совместим с коммутирующими скалярами из M и N: при любом SMulCommClass M N α CentroidHom α наследует SMulCommClass M N.

LaTeX

$$SMulCommClass M N (CentroidHom α)$$

Lean4

instance instSMul : SMul M (CentroidHom α) where
  smul n
    f :=
    {
      (n • f :
        α →+
          α) with
      map_mul_left' := fun a b ↦ by
        change n • f (a * b) = a * n • f b
        rw [map_mul_left f, ← mul_smul_comm]
      map_mul_right' := fun a b ↦ by
        change n • f (a * b) = n • f a * b
        rw [map_mul_right f, ← smul_mul_assoc] }

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