coprod_comp_prod — Mathlib

English

Replacing the right map by zero in coprod yields the left map composed with fst: f ∘ fst.

Русский

Замена правого отображения нулём в coprod даёт отображение f после fst: f ∘ fst.

LaTeX

$$$ f\\coprod (0) = f \\circ (fst\\ R\\ M\\ M_2) $$$

Lean4

@[simp]
theorem coprod_comp_prod (f : M₂ →ₗ[R] M₄) (g : M₃ →ₗ[R] M₄) (f' : M →ₗ[R] M₂) (g' : M →ₗ[R] M₃) :
    (f.coprod g).comp (f'.prod g') = f.comp f' + g.comp g' :=
  rfl

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