Triangulated

Statistics

Metric	Count
Definitions	0
Theorems `instIsTriangulatedOpposite`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTriangulatedOpposite` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.IsTriangulated` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instPreadditiveOpposite` `CategoryTheory.Limits.hasZeroObject_op` `instHasShiftOppositeInt` `instAdditiveOppositeShiftFunctorInt` `instOpposite`	—	`CategoryTheory.Limits.hasZeroObject_op` `instAdditiveOppositeShiftFunctorInt` `CategoryTheory.Pretriangulated.mem_distTriang_op_iff` `CategoryTheory.Triangulated.Octahedron'.comm₄` `CategoryTheory.Triangulated.Octahedron'.comm₃` `CategoryTheory.Functor.map_injective` `CategoryTheory.Functor.IsEquivalence.faithful` `CategoryTheory.instIsEquivalenceShiftFunctor` `CategoryTheory.NatIso.cancel_natIso_inv_right` `CategoryTheory.Functor.map_comp` `CategoryTheory.op_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Triangulated.Octahedron'.comm₁` `CategoryTheory.Triangulated.Octahedron'.comm₂` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality` `CategoryTheory.Pretriangulated.op_distinguished` `CategoryTheory.Triangulated.Octahedron'.mem` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_shift` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality_assoc` `CategoryTheory.Iso.inv_hom_id_app_assoc`

---