NegOnePow

Statistics

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_negOnePow` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Units.val` `instMonoid` `negOnePow` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`even_or_odd'` `negOnePow_two_mul` `cast_one` `zpow_mul` `zpow_ofNat` `Even.neg_pow` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `one_zpow` `zpow_add_one₀` `NeZero.one` `DivisionRing.toNontrivial` `negOnePow_two_mul_add_one` `cast_neg` `mul_neg` `mul_one`

---