instIntSMul — Mathlib

English

If M has Zero and N is an AddGroup, then there is a natural integer action on AddMonoidHom M N by a • f with (a • f)(m) = a • f(m).

Русский

Если M имеет ноль и N является AddGroup, то существует целочисленное действие на AddMonoidHom M N: (a·f)(m)=a·f(m).

LaTeX

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

Lean4

instance instIntSMul [AddZeroClass M] [AddCommGroup N] : SMul ℤ (M →+ N) where
  smul a
    f :=
    { toFun := a • f
      map_zero' := by simp [zsmul_zero]
      map_add' x y := by simp [zsmul_add] }

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