coprod_inr — Mathlib

English

Same statement as above: the coprod of inl and inr is the identity on the product.

Русский

То же самое: копродукт inl и inr равен тождественному отображению на произведении.

LaTeX

$$$ coprod (inl\\ R\\ M\\ M_2) (inr\\ R\\ M\\ M_2) = \\mathrm{id}_{M\\times M_2} $$$

Lean4

@[simp]
theorem coprod_inr (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : (coprod f g).comp (inr R M M₂) = g := by ext;
  simp only [map_zero, coprod_apply, inr_apply, zero_add, comp_apply]

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