Documentation Verification Report

Triangulated

📁 Source: Mathlib/CategoryTheory/Triangulated/Opposite/Triangulated.lean

Statistics

Metric	Count
Definitions	0
Theorems `instIsTriangulatedOpposite`	1
Total	1

CategoryTheory.Pretriangulated.Opposite

Theorems

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.Pretriangulated.rot_of_distTriang` `CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁` `CategoryTheory.IsTriangulated.mk'` `CategoryTheory.Limits.hasZeroObject_op` `instAdditiveOppositeShiftFunctorInt` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Pretriangulated.mem_distTriang_op_iff` `CategoryTheory.Pretriangulated.isomorphic_distinguished` `CategoryTheory.Functor.map_id` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv` `CategoryTheory.Functor.map_surjective` `CategoryTheory.Functor.IsEquivalence.full` `CategoryTheory.instIsEquivalenceShiftFunctor` `CategoryTheory.Functor.map_injective` `CategoryTheory.Functor.IsEquivalence.faithful` `CategoryTheory.Functor.map_comp` `CategoryTheory.Preadditive.comp_neg` `CategoryTheory.Preadditive.neg_comp` `CategoryTheory.Triangulated.Octahedron.comm₄` `CategoryTheory.Triangulated.Octahedron.comm₃` `CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc` `CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop` `Quiver.Hom.unop_op` `CategoryTheory.Triangulated.Octahedron.comm₂` `CategoryTheory.Triangulated.Octahedron.comm₁` `CategoryTheory.unop_comp_assoc` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality` `CategoryTheory.Pretriangulated.Triangle.shift_distinguished_iff` `CategoryTheory.Pretriangulated.mem_distTriang_op_iff'` `CategoryTheory.Triangulated.Octahedron.mem` `neg_add_cancel` `Int.negOnePow_neg` `Units.neg_smul` `one_smul` `CategoryTheory.NatTrans.naturality` `neg_neg` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_neg` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Pretriangulated.shiftFunctor_op_map` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Iso.inv_hom_id_app_assoc` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality_assoc`

---

← Back to Index