Documentation Verification Report

Power

📁 Source: Mathlib/Algebra/Order/Field/Power.lean

Statistics

Metric	Count
Definitions `evalZPow`	1
Theorems `zpow_abs`, `zpow_nonneg`, `zpow_pos`, `zpow_pos_iff`, `cast_le_pow_div_sub`, `cast_le_pow_sub_div_sub`, `zpow_neg`, `zpow_neg_iff`, `zpow_nonneg_iff`, `zpow_nonpos`, `zpow_nonpos_iff`, `zpow_pos_iff`, `abs_neg_one_zpow`, `abs_zpow`, `zpow_eq_neg_one_iff₀`, `zpow_eq_neg_zpow_iff₀`, `zpow_eq_one_iff_cases₀`, `zpow_eq_one_iff_of_ne_zero₀`, `zpow_eq_zpow_iff_cases₀`, `zpow_eq_zpow_iff_of_ne_zero₀`, `zpow_neg_two_nonneg`, `zpow_two_nonneg`, `zpow_two_pos_of_ne_zero`	23
Total	24

Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zpow_abs` 📖	mathematical	`Even`	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`abs_choice` `neg_zpow`
`zpow_nonneg` 📖	mathematical	`Even`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`zpow_add'` `IsDomain.to_noZeroDivisors` `Int.instIsDomain` `Int.instCharZero` `mul_self_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid`
`zpow_pos` 📖	mathematical	`Even`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`LE.le.lt_of_ne'` `zpow_nonneg` `zpow_ne_zero`
`zpow_pos_iff` 📖	mathematical	`Even`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`zpow_add'` `IsDomain.to_noZeroDivisors` `Int.instIsDomain` `Int.instCharZero` `mul_self_pos` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toMulPosStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `contravariant_lt_of_covariant_le` `zpow_ne_zero_iff`

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalZPow` 📖	CompOp	—

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_le_pow_div_sub` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`Preorder.toLE` `AddMonoidWithOne.toNatCast` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`LE.le.trans` `cast_le_pow_sub_div_sub` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `sub_le_self` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `zero_le_one` `IsStrictOrderedRing.toZeroLEOneClass` `sub_nonneg` `covariant_swap_add_of_covariant_add` `LT.lt.le`
`cast_le_pow_sub_div_sub` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`Preorder.toLE` `AddMonoidWithOne.toNatCast` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `le_sub_left_of_add_le` `one_add_mul_sub_le_pow` `LE.le.trans` `neg_le_self` `zero_le_one` `IsStrictOrderedRing.toZeroLEOneClass` `LT.lt.le`

Odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zpow_neg` 📖	mathematical	`Odd` `Int.instSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`zpow_neg_iff`
`zpow_neg_iff` 📖	mathematical	`Odd` `Int.instSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`lt_imp_lt_of_le_imp_le` `zpow_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `zpow_add_one₀` `LT.lt.ne` `mul_neg_of_pos_of_neg` `Even.zpow_pos` `even_two_mul`
`zpow_nonneg_iff` 📖	mathematical	`Odd` `Int.instSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`le_iff_le_iff_lt_iff_lt` `zpow_neg_iff`
`zpow_nonpos` 📖	mathematical	`Odd` `Int.instSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`zpow_nonpos_iff`
`zpow_nonpos_iff` 📖	mathematical	`Odd` `Int.instSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`le_iff_lt_or_eq` `zpow_neg_iff` `zpow_eq_zero_iff` `Int.not_even_iff_odd` `Even.zero`
`zpow_pos_iff` 📖	mathematical	`Odd` `Int.instSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`lt_iff_lt_of_le_iff_le` `zpow_nonpos_iff`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_neg_one_zpow` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`abs_zpow` `abs_neg` `abs_one` `IsStrictOrderedRing.toIsOrderedRing` `one_zpow`
`abs_zpow` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid`	—	`map_zpow₀` `MonoidWithZeroHom.monoidWithZeroHomClass` `IsStrictOrderedRing.toIsOrderedRing`
`zpow_eq_neg_one_iff₀` 📖	mathematical	—	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Odd` `Int.instSemiring`	—	`one_zpow` `zpow_eq_neg_zpow_iff₀` `one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`zpow_eq_neg_zpow_iff₀` 📖	mathematical	—	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Odd` `Int.instSemiring`	—	`zpow_natCast` `zpow_neg` `pow_eq_neg_pow_iff` `Nat.cast_add` `Nat.cast_one` `neg_add_rev`
`zpow_eq_one_iff_cases₀` 📖	mathematical	—	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Even`	—	`one_zpow`
`zpow_eq_one_iff_of_ne_zero₀` 📖	mathematical	—	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Even`	—	`zpow_eq_zpow_iff_of_ne_zero₀` `one_zpow`
`zpow_eq_zpow_iff_cases₀` 📖	mathematical	—	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Even`	—	`eq_or_ne` `zpow_zero`
`zpow_eq_zpow_iff_of_ne_zero₀` 📖	mathematical	—	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Even`	—	`zpow_natCast` `pow_eq_pow_iff_of_ne_zero` `Int.instCharZero` `zpow_neg`
`zpow_neg_two_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`Even.zpow_nonneg` `Nat.instAtLeastTwoHAddOfNat` `even_neg_two`
`zpow_two_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`Even.zpow_nonneg` `Nat.instAtLeastTwoHAddOfNat` `even_two`
`zpow_two_pos_of_ne_zero` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`Even.zpow_pos` `Nat.instAtLeastTwoHAddOfNat` `even_two`

---

← Back to Index