Powers of -1 in the center of a preadditive category #
@[simp]
theorem
CategoryTheory.CatCenter.app_neg_one_zpow
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(n : ℤ)
(X : C)
:
-1 in the center of a preadditive category #