coproductCocone_inl — Mathlib

English

In the coproduct cocone of CommRingCat, the left leg corresponds to the inclusion from the left tensor factor (via the ℤ-entry).

Русский

В коконе coproductCocone для CommRingCat левая ножка соответствует включению левой тензорной части через ℤ.

LaTeX

$$$(coproductCocone A B).inl = \mathrm{ofHom}(\text{Algebra.TensorProduct.includeLeft} (S := \mathbb{Z})).\toRingHom$$

Lean4

@[simp]
theorem coproductCocone_inl :
    (coproductCocone A B).inl = ofHom (Algebra.TensorProduct.includeLeft (S := ℤ)).toRingHom :=
  rfl

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