intLinear — Mathlib

English

An additive functor F between preadditive categories is ℤ-linear, i.e., it preserves integer scalar multiplication on hom-sets.

Русский

Аддитивный функтор между преддобавительными категориями является ℤ-линейным, т.е. сохраняет умножение на целые числа на множества гомоморфизмов.

LaTeX

$$$F \\text{ is } \\mathbb{Z}\\text{-linear}$$$

Lean4

instance intLinear : F.Linear ℤ where map_smul f r := F.mapAddHom.map_zsmul f r

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