Theorems · Theorem · category theory

CommGrpCat.binaryProductLimitCone_isLimit_lift

∀ (G H : CommGrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)),
  (G.binaryProductLimitCone H).isLimit.lift t =
    CommGrpCat.ofHom
      ((CommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod
        (CommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))

Defined in: Mathlib.Algebra.Category.Grp.CartesianMonoidal
Cited by: 0 results in Mathlib
Foundations: Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites20

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement · cited by 32,603
CategoryTheory.Discretestatement · cited by 2,447
CategoryTheory.Limits.WalkingPairstatement · cited by 1,319
CategoryTheory.Limits.Cone.ptstatement · cited by 1,298
CategoryTheory.Limits.Conestatement and proof · cited by 710
CategoryTheory.Limits.pairstatement and proof · cited by 536
CategoryTheory.Limits.IsLimit.liftstatement and proof · cited by 167
CategoryTheory.Limits.BinaryFan.mkstatement · cited by 112
CommGrpCatstatement and proof · cited by 74
CommGrpCat.carrierstatement · cited by 59
CategoryTheory.Limits.LimitCone.isLimitstatement and proof · cited by 58
CategoryTheory.Limits.BinaryFan.sndstatement · cited by 53

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.