coprod_add — Mathlib

English

The coprod of sums distributes: (f1+g1) coprod (f2+g2) = f1 coprod f2 + g1 coprod g2.

Русский

Копрод сумм распределяется: (f1+g1) coprod (f2+g2) = f1 coprod f2 + g1 coprod g2.

LaTeX

$$$$ (f_1+g_1).coprod (f_2+g_2) = f_1.coprod f_2 + g_1.coprod g_2 $$$$

Lean4

@[simp]
theorem coprod_add (f₁ g₁ : M₁ →L[R] M) (f₂ g₂ : M₂ →L[R] M) :
    (f₁ + g₁).coprod (f₂ + g₂) = f₁.coprod f₂ + g₁.coprod g₂ := by ext <;> simp

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