biprodIsoProd_inv_comp_snd — Mathlib

English

The inverse of the biproduct–product isomorphism composed with the second projection is the snd projection.

Русский

Обратное изоморфизма между бипродуктом и произведением, после проекции справа, даёт snd.

LaTeX

$$(biprodIsoProd G H)^{-1} \circ biprod.snd = ofHom (AddMonoidHom.snd G H)$$

Lean4

@[simp, elementwise]
theorem biprodIsoProd_inv_comp_snd (G H : AddCommGrpCat.{u}) :
    (biprodIsoProd G H).inv ≫ biprod.snd = ofHom (AddMonoidHom.snd G H) :=
  IsLimit.conePointUniqueUpToIso_inv_comp _ _ (Discrete.mk WalkingPair.right)

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