Documentation Verification Report

Pow

📁 Source: Mathlib/Data/ENat/Pow.lean

Statistics

Metric	Count
Definitions `instPow`	1
Theorems `epow_add`, `epow_eq_one_iff`, `epow_eq_zero_iff`, `epow_left_mono`, `epow_mul`, `epow_natCast`, `epow_one`, `epow_right_mono`, `epow_top`, `epow_zero`, `mul_epow`, `one_epow`, `one_le_epow`, `top_epow`, `top_epow_top`, `zero_epow`, `zero_epow_top`	17
Total	18

ENat

Definitions

Name	Category	Theorems
`instPow` 📖	CompOp	18 math math: `epow_natCast`, `top_epow`, `zero_epow`, `epow_mul`, `epow_add`, `epow_right_mono`, `top_epow_top`, `mul_epow`, `epow_one`, `epow_left_mono`, `epow_eq_one_iff`, `epow_eq_zero_iff`, `one_le_epow`, `card_fun`, `zero_epow_top`, `epow_top`, `epow_zero`, `one_epow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epow_add` 📖	mathematical	—	`ENat` `instPow` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Distrib.toMul`	—	`lt_trichotomy` `lt_one_iff_eq_zero` `eq_zero_or_pos` `zero_add` `epow_zero` `one_mul` `zero_epow` `LT.lt.ne` `MulZeroClass.zero_mul` `add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `bot_le` `one_epow` `mul_one` `top_add` `epow_top` `top_mul` `one_le_iff_ne_zero` `one_le_epow` `LT.lt.le` `add_top` `mul_top` `pow_add`
`epow_eq_one_iff` 📖	mathematical	—	`ENat` `instPow` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `instZeroENat`	—	`lt_trichotomy` `zero_epow` `lt_one_iff_eq_zero` `epow_right_mono` `one_le_iff_ne_zero` `LT.lt.le` `not_lt_of_ge` `epow_one` `one_epow` `epow_zero`
`epow_eq_zero_iff` 📖	mathematical	—	`ENat` `instPow` `instZeroENat`	—	`one_le_iff_ne_zero` `one_le_epow` `epow_zero` `zero_epow`
`epow_left_mono` 📖	mathematical	—	`Monotone` `ENat` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instPow`	—	`lt_trichotomy` `lt_one_iff_eq_zero` `zero_epow_top` `bot_le` `one_epow` `one_le_epow` `one_le_iff_ne_zero` `epow_top` `LT.lt.trans_le` `le_top` `pow_left_mono` `CanonicallyOrderedAdd.toMulLeftMono` `covariant_swap_mul_of_covariant_mul`
`epow_mul` 📖	mathematical	—	`ENat` `instPow` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`eq_or_ne` `MulZeroClass.zero_mul` `epow_zero` `one_epow` `MulZeroClass.mul_zero` `lt_trichotomy` `lt_one_iff_eq_zero` `zero_epow` `mul_ne_zero` `top_mul` `epow_top` `top_epow` `mul_top` `LE.le.trans_lt'` `epow_right_mono` `one_le_iff_ne_zero` `LT.lt.le` `epow_one` `pow_mul`
`epow_natCast` 📖	mathematical	—	`ENat` `instPow` `instNatCast` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiringENat`	—	—
`epow_one` 📖	mathematical	—	`ENat` `instPow` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`coe_one` `epow_natCast` `pow_one`
`epow_right_mono` 📖	mathematical	—	`Monotone` `ENat` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instPow`	—	`top_le_iff` `le_refl` `lt_trichotomy` `lt_one_iff_eq_zero` `one_epow` `epow_top` `pow_right_mono₀` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `one_le_iff_ne_zero` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid`
`epow_top` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`instPow` `Top.top` `instTopENat`	—	`LT.lt.ne` `LE.le.trans_lt` `zero_le_one` `IsOrderedRing.toZeroLEOneClass`
`epow_zero` 📖	mathematical	—	`ENat` `instPow` `instZeroENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`coe_zero` `epow_natCast` `pow_zero`
`mul_epow` 📖	mathematical	—	`ENat` `instPow` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`lt_trichotomy` `lt_one_iff_eq_zero` `MulZeroClass.zero_mul` `one_mul` `one_epow` `MulZeroClass.mul_zero` `mul_one` `epow_top` `WithTop.top_mul_top` `one_lt_mul` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toMulPosMono` `LT.lt.le` `mul_pow`
`one_epow` 📖	mathematical	—	`ENat` `instPow` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`epow_natCast` `one_pow`
`one_le_epow` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `instPow`	—	`epow_zero` `epow_right_mono` `zero_le`
`top_epow` 📖	mathematical	—	`ENat` `instPow` `Top.top` `instTopENat`	—	`top_epow_top` `epow_natCast` `pow_eq_top_iff` `Nat.cast_ne_zero`
`top_epow_top` 📖	mathematical	—	`ENat` `instPow` `Top.top` `instTopENat`	—	—
`zero_epow` 📖	mathematical	—	`ENat` `instPow` `instZeroENat`	—	`zero_epow_top` `epow_natCast` `pow_eq_zero_iff'` `isReduced_of_noZeroDivisors` `Nat.cast_ne_zero`
`zero_epow_top` 📖	mathematical	—	`ENat` `instPow` `instZeroENat` `Top.top` `instTopENat`	—	—

---

← Back to Index