instIntSMul — Mathlib

English

For Zero M and AddGroup N, there is a natural integer-scalar action on ZeroHom M N by a • f with (a • f)(m) = a • f(m).

Русский

Для Zero M и AddGroup N существует целочисленное действие на ZeroHom M N: (a • f)(m) = a • f(m).

LaTeX

$$$\mathbb{Z}\text{-action on }\mathrm{ZeroHom}(M,N),\; (a\cdot f)(m)=a\cdot f(m).$$$

Lean4

instance instIntSMul [Zero M] [AddGroup N] : SMul ℤ (ZeroHom M N) where
  smul a
    f :=
    { toFun := a • f
      map_zero' := by simp [zsmul_zero] }

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