instSMulNatHom — Mathlib

English

There is a natural-number scalar action on Hom(X,Y): n • f is a morphism with hom equal to n • f.hom.

Русский

Существует масштабирование натурального числа на отображениях: n • f — это морфизм, у которого компонент Hom равен n • f.hom.

LaTeX

$$$\\mathrm{SMul}_{\\mathbb{N}}(\\operatorname{Hom}_{Action}(X,Y))$$$

Lean4

instance : SMul ℕ (X ⟶ Y) where smul n f := ⟨n • f.hom, by simp [f.comm]⟩

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