English
Let f: X →* Y and g: Y →* Z be commutative-group homomorphisms. Then the morphism corresponding to the composite g ∘ f is the composition of the corresponding morphisms: ofHom(g ∘ f) = ofHom(f) ≫ ofHom(g).
Русский
Пусть f: X →* Y и g: Y →* Z — гомоморфизмы групп. Тогда мороморфизм, соответствующий композиции g ∘ f, равен композиции соответствующих мороморфизмов: ofHom(g ∘ f) = ofHom(f) ∘ ofHom(g).
LaTeX
$$$$ \forall X,Y,Z\,[\mathrm{CommGroup}(X)], [\mathrm{CommGroup}(Y)], [\mathrm{CommGroup}(Z)], \ (f : X \to_* Y) (g : Y \to_* Z),\quad \mathrm{ofHom}(g \cdot f) = (\mathrm{ofHom}(f)) \circ (\mathrm{ofHom}(g)). $$$$
Lean4
@[to_additive (attr := simp)]
theorem ofHom_comp {X Y Z : Type u} [CommGroup X] [CommGroup Y] [CommGroup Z] (f : X →* Y) (g : Y →* Z) :
ofHom (g.comp f) = ofHom f ≫ ofHom g :=
rfl
