prodMap_add — Mathlib

English

The prodMap distributes over addition: (f1+f2).prodMap (g1+g2) = f1.prodMap g1 + f2.prodMap g2.

Русский

ProdMap распадается по сложению: (f1+f2).prodMap(g1+g2) = f1.prodMap g1 + f2.prodMap g2.

LaTeX

$$$ (f_1 + f_2) \\text{ prodMap} (g_1 + g_2) = f_1 \\text{ prodMap } g_1 + f_2 \\text{ prodMap } g_2. $$$

Lean4

theorem prodMap_add (f₁ : M →ₗ[R] M₃) (f₂ : M →ₗ[R] M₃) (g₁ : M₂ →ₗ[R] M₄) (g₂ : M₂ →ₗ[R] M₄) :
    (f₁ + f₂).prodMap (g₁ + g₂) = f₁.prodMap g₁ + f₂.prodMap g₂ :=
  rfl

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