pushoutCocone_inl — Mathlib

English

The left leg (inl) of the pushout cocone equals the canonical inclusion of the left tensor factor.

Русский

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

LaTeX

$$$(\text{pushoutCocone } R A B).inl = \mathrm{ofHom}(\text{Algebra.TensorProduct.includeLeftRingHom}(A:=A))$$$

Lean4

@[simp]
theorem pushoutCocone_inl : (pushoutCocone R A B).inl = ofHom (Algebra.TensorProduct.includeLeftRingHom (A := A)) :=
  rfl

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