coprod_comp_inl_inr — Mathlib

English

Same statement as above with alternate notation; the image of the product submodule under coprod equals the join of the images.

Русский

То же самое утверждение, что и выше, с другой нотацией; изображение произведения подмодулей под coprod равно объединению изображений.

LaTeX

$$$ (Submodule.map (f.coprod g) (S.prod S')) = (S.map f) \\sqcup (S'.map g) $$$

Lean4

@[simp]
theorem coprod_comp_inl_inr (f : M × M₂ →ₗ[R] M₃) : (f.comp (inl R M M₂)).coprod (f.comp (inr R M M₂)) = f := by
  rw [← comp_coprod, coprod_inl_inr, comp_id]

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