pushoutCocone_inr — Mathlib

English

The right leg (inr) of the pushout cocone equals the canonical inclusion of the right tensor factor.

Русский

Правая ножка кокона пуш-аут равна каноническому включению правого тензор-фактора.

LaTeX

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

Lean4

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

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