ofHom_comp — Mathlib

English

The composition of two morphisms corresponds under ofHom to the composition of their images: ofHom(g ∘ f) = ofHom(f) ≫ ofHom(g).

Русский

Сведение композиции морфизмов через ofHom соответствует композиции их образов: ofHom(g ∘ f) = ofHom(f) ≫ ofHom(g).

LaTeX

$$$ \\mathrm{ofHom}(g \\circ f) = \\mathrm{ofHom}(f) \\; \\circ \\; \\mathrm{ofHom}(g). $$$

Lean4

@[simp]
theorem ofHom_comp {M N O : Type v} [AddCommGroup M] [AddCommGroup N] [AddCommGroup O] [Module R M] [Module R N]
    [Module R O] (f : M →ₗ[R] N) (g : N →ₗ[R] O) : ofHom (g.comp f) = ofHom f ≫ ofHom g :=
  rfl

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