hasIntScalar — Mathlib

English

There is a natural Z-module structure on the Hom set between two homological complexes, given by n • f with (n • f).f i = n • f.f i for all i.

Русский

Существует структура Z-модуля на множестве гомоморфизмов между гомологических комплексами: n • f действует по формуле (n • f).f i = n • f.f i для всех i.

LaTeX

$$$\text{instance } hasIntScalar : \mathrm{SMul} \mathbb{Z} (C \to D)$ with $((n \cdot f).f i) = n \cdot f.f i$$$

Lean4

instance hasIntScalar : SMul ℤ (C ⟶ D) :=
  ⟨fun n f =>
    { f := fun i => n • f.f i
      comm' := fun i j _ => by simp [Preadditive.zsmul_comp, Preadditive.comp_zsmul] }⟩

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