prodMap_comp — Mathlib

English

Product maps respect composition: composing prodMaps is the same as prodMap of the composed maps.

Русский

Отображения произведения сохраняют композицию: композиция prodMap равна prodMap от композиции отображений.

LaTeX

$$$ (f_{12} \\text{ prodMap } g_{12}) \\circ (f_{23} \\text{ prodMap } g_{23}) = (f_{23} \\circ f_{12}) \\text{ prodMap } (g_{23} \\circ g_{12}). $$$

Lean4

theorem prodMap_comp (f₁₂ : M →ₗ[R] M₂) (f₂₃ : M₂ →ₗ[R] M₃) (g₁₂ : M₄ →ₗ[R] M₅) (g₂₃ : M₅ →ₗ[R] M₆) :
    f₂₃.prodMap g₂₃ ∘ₗ f₁₂.prodMap g₁₂ = (f₂₃ ∘ₗ f₁₂).prodMap (g₂₃ ∘ₗ g₁₂) :=
  rfl

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