NegOnePow

Statistics

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` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsMulCommutative.instCommRing` `CategoryTheory.Preadditive.instRingEnd` `CategoryTheory.functorCategoryPreadditive` `instIsMulCommutative` `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`	—	`instIsMulCommutative` `Int.even_or_odd` `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`

---