ofHom_comp — Mathlib

English

The construction of OfHom preserves composition: for f : X →* Y and g : Y →* Z, we have ofHom (g ∘ f) = ofHom f ∘ ofHom g.

Русский

Конструкция OfHom сохраняет композицию: для гомоморфизмов f : X →* Y и g : Y →* Z выполняется ofHom (g ∘ f) = ofHom f ∘ ofHom g.

LaTeX

$$$ \\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} [Group X] [Group Y] [Group Z] (f : X →* Y) (g : Y →* Z) :
    ofHom (g.comp f) = ofHom f ≫ ofHom g :=
  rfl

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