NegOnePow

📁 Source: Mathlib/CategoryTheory/Center/NegOnePow.lean

Statistics

Metric	Count
Definitions	0
Theorems app_neg_one_zpow	1
Total	1

CategoryTheory.CatCenter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_neg_one_zpow 📖	mathematical	—	app Units.val CategoryTheory.CatCenter CategoryTheory.End.monoid CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id Units DivInvMonoid.toZPow Units.instDivInvMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd CategoryTheory.functorCategoryPreadditive Units.instOne Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow CategoryTheory.CategoryStruct.id	—	Int.even_or_odd instIsMulCommutative zpow_add mul_neg mul_one neg_neg one_zpow Int.negOnePow_even Even.add_self one_smul Int.negOnePow_odd odd_two_mul_add_one zpow_one neg_smul

---

← Back to Index