coproductCocone_inr — Mathlib

English

In the coproduct cocone of CommRingCat, the right leg corresponds to the inclusion from the right tensor factor.

Русский

В коконе coproductCocone левая/правый отложены включения из правого тензорного фактора.

LaTeX

$$$(coproductCocone A B).inr = \mathrm{ofHom}(\text{Algebra.TensorProduct.includeRight} (R := \mathbb{Z})).\toRingHom$$

Lean4

@[simp]
theorem coproductCocone_inr :
    (coproductCocone A B).inr = ofHom (Algebra.TensorProduct.includeRight (R := ℤ)).toRingHom :=
  rfl

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