binaryProductLimitCone_cone_π_app_right

English

The right projection in the binary product limit cone equals the second projection map provided by LinearMap.snd.

Русский

Правая проекция в ограничении произведения равна snd.

LaTeX

$$$(binaryProductLimitCone M N).cone.\pi.app\langle WalkingPair.right \rangle = \mathrm{ofHom}(\mathrm{LinearMap.snd}\;R\;M\;N)$$$

Lean4

@[simp]
theorem binaryProductLimitCone_cone_π_app_right (M N : ModuleCat.{v} R) :
    (binaryProductLimitCone M N).cone.π.app ⟨WalkingPair.right⟩ = ofHom (LinearMap.snd R M N) :=
  rfl

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