Theorems · Theorem · category theory
AddCommGrpCat.biprodIsoProd_inv_comp_fst_apply
∀ (G H : AddCommGrpCat) (x : ↑G × ↑H),
(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.biprod.fst)
((CategoryTheory.ConcreteCategory.hom (G.biprodIsoProd H).inv) x) =
x.1- Defined in
- Mathlib.Algebra.Category.Grp.Biproducts
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CategoryTheory.Iso.invstatement and proof · cited by 6,514
- CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
- AddMonoidHomstatement · cited by 3,230
- AddCommGrpCatstatement and proof · cited by 462
- AddCommGrpCat.carrierstatement and proof · cited by 407
- CategoryTheory.comp_applyproof · cited by 387
- CategoryTheory.Limits.biprodstatement · cited by 312
- CategoryTheory.ConcreteCategory.hom_ofHomproof · cited by 205
- CategoryTheory.Limits.biprod.fststatement and proof · cited by 121
- AddCommGrpCat.ofstatement · cited by 97
- AddCommGrpCat.ofHomproof · cited by 72
Cited by1
Results whose statement or proof uses this declaration.
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_applyproof · cited by 1