Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Order/Ring/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `add_pow_le`, `pow_nonneg`, `pow_pos`, `pow_pos_iff`, `nonneg`, `pow_inj`, `pow_injective`, `pow_le_pow`, `pow_lt_pow`, `pow_neg`, `pow_neg_iff`, `pow_nonneg_iff`, `pow_nonpos`, `pow_nonpos_iff`, `pow_pos_iff`, `strictMono_pow`, `add_pow_le`, `add_sq_le`, `not_isSquare_of_neg`, `pow_add_pow_le`, `pow_add_pow_le'`, `pow_four_le_pow_two_of_pow_two_le`, `pow_two_pos_of_ne_zero`, `sq_pos_iff`, `sq_pos_of_ne_zero`, `sq_pos_of_neg`	26
Total	26

Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_pow_le` 📖	mathematical	`Even`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `two_mul` `pow_mul` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toMulPosMono` `sq_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `add_sq_le` `Commute.mul_pow` `mul_two` `mul_le_mul_of_nonneg_left` `add_pow_le` `pow_nonneg` `IsStrictOrderedRing.toZeroLEOneClass` `zero_le_two`
`pow_nonneg` 📖	mathematical	`Even`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_add` `mul_self_nonneg` `IsOrderedRing.toPosMulMono` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid`
`pow_pos` 📖	mathematical	`Even`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`LE.le.lt_of_ne'` `pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `IsStrictOrderedRing.isDomain`
`pow_pos_iff` 📖	mathematical	`Even`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_add` `mul_self_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toMulPosStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `contravariant_lt_of_covariant_le` `pow_ne_zero_iff` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `IsStrictOrderedRing.isDomain`

IsSquare

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonneg` 📖	mathematical	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`mul_self_nonneg`

Odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_inj` 📖	mathematical	`Odd` `Nat.instSemiring`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_injective`
`pow_injective` 📖	mathematical	`Odd` `Nat.instSemiring`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`StrictMono.injective` `strictMono_pow`
`pow_le_pow` 📖	mathematical	`Odd` `Nat.instSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`StrictMono.le_iff_le` `strictMono_pow`
`pow_lt_pow` 📖	mathematical	`Odd` `Nat.instSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`StrictMono.lt_iff_lt` `strictMono_pow`
`pow_neg` 📖	mathematical	`Odd` `Nat.instSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_neg_iff`
`pow_neg_iff` 📖	mathematical	`Odd` `Nat.instSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`lt_imp_lt_of_le_imp_le` `pow_nonneg` `IsStrictOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `pow_succ` `mul_neg_of_pos_of_neg` `IsStrictOrderedRing.toPosMulStrictMono` `Even.pow_pos` `Nat.instAtLeastTwoHAddOfNat` `even_two_mul` `LT.lt.ne`
`pow_nonneg_iff` 📖	mathematical	`Odd` `Nat.instSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`le_iff_le_iff_lt_iff_lt` `pow_neg_iff`
`pow_nonpos` 📖	mathematical	`Odd` `Nat.instSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_nonpos_iff`
`pow_nonpos_iff` 📖	mathematical	`Odd` `Nat.instSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`le_iff_lt_or_eq` `pow_neg_iff` `pow_eq_zero_iff` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `IsStrictOrderedRing.isDomain` `Nat.instIsDomain` `Nat.instCharZero`
`pow_pos_iff` 📖	mathematical	`Odd` `Nat.instSemiring`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`lt_iff_lt_of_le_iff_le` `pow_nonpos_iff`
`strictMono_pow` 📖	mathematical	`Odd` `Nat.instSemiring`	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`IsDomain.to_noZeroDivisors` `Nat.instIsDomain` `Nat.instCharZero` `le_total` `pow_lt_pow_left₀` `IsStrictOrderedRing.toPosMulStrictMono` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `lt_or_ge` `LE.le.trans_lt` `pow_nonpos` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `ExistsAddOfLE.exists_add_of_le` `nonneg_of_le_add_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `LE.le.trans_eq` `lt_of_add_lt_add_right` `contravariant_swap_add_of_contravariant_add` `add_assoc` `pow_add_pow_eq_zero` `zero_add` `add_rotate'` `add_zero` `add_left_comm`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_pow_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `pow_zero` `Nat.instZeroLEOneClass` `one_mul` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsStrictOrderedRing.toZeroLEOneClass` `pow_one` `pow_succ` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `add_nonneg` `mul_assoc` `mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass` `add_comm` `add_add_add_comm` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `add_le_add_right` `le_total` `mul_add_mul_le_mul_add_mul` `pow_le_pow_left₀` `mul_add_mul_le_mul_add_mul'` `pow_nonneg` `zero_le_two`
`add_sq_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `pow_succ'` `pow_zero` `mul_one` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `add_comm` `add_add_add_comm` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `le_total` `mul_add_mul_le_mul_add_mul` `IsOrderedRing.toMulPosMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `mul_add_mul_le_mul_add_mul'` `two_mul`
`not_isSquare_of_neg` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`LT.lt.not_ge` `IsSquare.nonneg`
`pow_add_pow_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`zero_add` `pow_one` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `mul_nonneg` `IsOrderedRing.toPosMulMono` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `pow_succ'` `le_add_of_nonneg_right` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `add_comm` `add_assoc` `mul_le_mul_of_nonneg_left`
`pow_add_pow_le'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `two_mul` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `le_add_of_nonneg_right` `le_add_of_nonneg_left`
`pow_four_le_pow_two_of_pow_two_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—	`pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `sq_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `pow_mul`
`pow_two_pos_of_ne_zero` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`sq_pos_of_ne_zero`
`sq_pos_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Even.pow_pos_iff` `Nat.instAtLeastTwoHAddOfNat` `even_two` `two_ne_zero`
`sq_pos_of_ne_zero` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`sq_pos_iff`
`sq_pos_of_neg` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`sq` `mul_pos_of_neg_of_neg` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `contravariant_swap_add_of_contravariant_add` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid`

---

← Back to Index