instSMulCommClassUniformFun — Mathlib

English

If scalar actions by M and N commute on β (SMulCommClass M N β), then they commute on the function space UniformFun α β; i.e., SMulCommClass M N (UniformFun α β).

Русский

Если скалярные действия M и N на β коммутируют (SMulCommClass M N β), то они же коммутируют на пространстве функций UniformFun α β.

LaTeX

$$$SMulCommClass\; M\; N\; β \rightarrow SMulCommClass\; M\; N\; (\mathrm{UniformFun} \; α \; β).$$$

Lean4

instance {M N : Type*} [SMul M β] [SMul N β] [SMulCommClass M N β] : SMulCommClass M N (α →ᵤ β) :=
  Pi.smulCommClass

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