Mathlib Map

Theorems · Theorem · category theory

AddCommGrpCat.biprodIsoProd_inv_comp_snd

∀ (G H : AddCommGrpCat),
  CategoryTheory.CategoryStruct.comp (G.biprodIsoProd H).inv CategoryTheory.Limits.biprod.snd =
    AddCommGrpCat.ofHom (AddMonoidHom.snd ↑G ↑H)
Defined in
Mathlib.Algebra.Category.Grp.Biproducts
Cited by
1 results in Mathlib
Foundations
Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AddCommGrpCat.biprodIsoProd_inv_comp_snd_apply · cited by 1AddCommGrpCat.biprodIsoPr…Quiver.Hom · cited by 32603Quiver.HomCategoryTheory.CategoryStruct.comp · cited by 17999CategoryStruct.compCategoryTheory.Iso.inv · cited by 6514Iso.invAddCommGrpCat · cited by 462AddCommGrpCatAddCommGrpCat.carrier · cited by 407AddCommGrpCat.carrierCategoryTheory.Limits.biprod · cited by 312Limits.biprodCategoryTheory.Limits.biprod.snd · cited by 132biprod.sndAddCommGrpCat.of · cited by 97AddCommGrpCat.ofAddCommGrpCat.ofHom · cited by 72AddCommGrpCat.ofHomCategoryTheory.Limits.LimitCone.isLimit · cited by 58LimitCone.isLimitAddMonoidHom.snd · cited by 42AddMonoidHom.sndCategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp · cited by 37IsLimit.conePointUniqueUp…CategoryTheory.Limits.BinaryBiproduct.isLimit · cited by 14BinaryBiproduct.isLimitAddCommGrpCat.biprodIsoProd · cited by 10AddCommGrpCat.biprodIsoPr…AddCommGrpCat.binaryProductLimitCone · cited by 6AddCommGrpCat.binaryProdu…AddCommGrpCat.biprodIsoProd_i…CITED BYCITES

Cites15

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

Cited by1

Results whose statement or proof uses this declaration.