prodMap_mul — Mathlib

English

Product maps respect multiplication: the product of prodMap maps equals the prodMap map of products.

Русский

Произведение prodMap отображений равно prodMap отображения для произведений отображений.

LaTeX

$$$ f_2 \\text{ prodMap } g_2 \\; * \\; f_1 \\text{ prodMap } g_1 = (f_2 \\cdot f_1) \\text{ prodMap } (g_2 \\cdot g_1). $$$

Lean4

theorem prodMap_mul (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

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