instSMulNatHom — Mathlib

English

There is a canonical action of natural numbers on Hom-sets in AddCommGrpCat given by scaling the morphism's underlying hom.

Русский

Для множеств гомоморфизмов в AddCommGrpCat задано естественное действие натуральных чисел на Hom через умножение базового гомоморфа.

LaTeX

$$$\\operatorname{SMul}(\\mathbb{N}, \\mathrm{Hom})$$$

Lean4

instance : SMul ℕ (M ⟶ N) where smul n f := ofHom (n • f.hom)

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