Power

Statistics

Metric	Count
Definitions	0
Theorems `neg_one_zpow`, `neg_zpow`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`neg_one_zpow` 📖	mathematical	`Odd` `Int.instSemiring`	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`neg_zpow` `one_zpow`
`neg_zpow` 📖	mathematical	`Odd` `Int.instSemiring`	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing`	—	`Int.not_even_iff_odd` `Even.zero` `zpow_add'` `zpow_one` `zpow_mul` `zpow_two` `neg_mul_neg` `neg_mul_eq_mul_neg`

---