coprod_comp_inr — Mathlib

English

Another facet of the same equivalence, showing compatibility with the projection to each component.

Русский

Дополнительное свойство той же эквивалентности, демонстрирующее совместимость с проекцией на каждую компоненту.

LaTeX

$$$$ \text{coprodEquiv}({f})_{\text{fst}} = f_{\text{fst}} \circ \mathrm{coprod} $$$$

Lean4

@[simp]
theorem coprod_comp_inr (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) : (f₁.coprod f₂).comp (.inr _ _ _) = f₂ :=
  coe_injective <| LinearMap.coprod_inr ..

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