Pow

📁 Source: Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean

Statistics

Metric	Count
Definitions	0
Theorems `nsmul_neg`, `nsmul_neg_iff`, `nsmul_nonneg`, `nsmul_nonpos`, `one_le_pow_of_le`, `pow_le_one_of_le`, `pow_lt_one_iff`, `pow_lt_one_iff'`, `pow_lt_one_of_lt`, `const_nsmul`, `pow_const`, `nsmul_neg`, `nsmul_neg_iff`, `nsmul_nonneg`, `nsmul_nonpos`, `one_le_pow_of_le`, `pow_le_one_of_le`, `pow_lt_one_iff`, `pow_lt_one_of_lt`, `const_nsmul`, `pow_const`, `instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono`, `instIsMulTorsionFreeOfMulLeftStrictMonoOfMulRightStrictMono`, `le_max_of_sq_le_mul`, `le_max_of_two_nsmul_le_add`, `le_of_nsmul_le_nsmul_right`, `le_of_pow_le_pow_left'`, `le_pow_sup`, `le_self_nsmul`, `le_self_pow`, `lt_max_of_sq_lt_mul`, `lt_max_of_two_nsmul_lt_add`, `lt_of_nsmul_lt_nsmul_right`, `lt_of_pow_lt_pow_left'`, `min_le_of_add_le_two_nsmul`, `min_le_of_mul_le_sq`, `min_lt_of_add_lt_two_nsmul`, `min_lt_of_mul_lt_sq`, `nsmul_le_nsmul`, `nsmul_le_nsmul_add_of_sq_le_add`, `nsmul_le_nsmul_iff_left`, `nsmul_le_nsmul_iff_right`, `nsmul_le_nsmul_left`, `nsmul_le_nsmul_left_of_nonpos`, `nsmul_le_nsmul_right`, `nsmul_left_monotone`, `nsmul_left_strictMono`, `nsmul_lt_nsmul_iff_left`, `nsmul_lt_nsmul_left`, `nsmul_lt_nsmul_right`, `nsmul_neg`, `nsmul_neg_iff`, `nsmul_nonneg`, `nsmul_nonneg_iff`, `nsmul_nonpos`, `nsmul_nonpos_iff`, `nsmul_pos`, `nsmul_pos_iff`, `nsmul_right_mono`, `nsmul_right_strictMono`, `one_le_pow_iff`, `one_le_pow_of_one_le'`, `one_le_zpow`, `one_lt_pow'`, `one_lt_pow_iff`, `one_lt_zpow`, `pow_inf_le`, `pow_le_one'`, `pow_le_one_iff`, `pow_le_pow`, `pow_le_pow_iff_left`, `pow_le_pow_iff_right'`, `pow_le_pow_left'`, `pow_le_pow_mul_of_sq_le_mul`, `pow_le_pow_right'`, `pow_le_pow_right_of_le_one'`, `pow_left_mono`, `pow_left_strictMono`, `pow_lt_one'`, `pow_lt_one_iff`, `pow_lt_pow_iff_right'`, `pow_lt_pow_left'`, `pow_lt_pow_right'`, `pow_right_monotone`, `pow_right_strictMono'`, `zsmul_nonneg`, `zsmul_pos`	87
Total	87

Left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nsmul_neg` 📖	mathematical	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLT` `AddMonoid.toNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`succ_nsmul'` `add_neg_of_neg_of_nonpos` `nsmul_nonpos` `LT.lt.le`
`nsmul_neg_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`nsmul_neg_iff` `addLeftMono_of_addLeftStrictMono` `LT.lt.ne'`
`nsmul_nonneg` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`zero_nsmul` `instReflLe` `succ_nsmul` `add_nonneg`
`nsmul_nonpos` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `AddMonoid.toNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`nsmul_nonneg` `OrderDual.addLeftMono`
`one_le_pow_of_le` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`pow_zero` `instReflLe` `pow_succ` `one_le_mul`
`pow_le_one_of_le` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `Monoid.toPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`one_le_pow_of_le` `OrderDual.mulLeftMono`
`pow_lt_one_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`pow_lt_one_iff'`
`pow_lt_one_iff'` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`pow_lt_one_iff` `mulLeftMono_of_mulLeftStrictMono` `LT.lt.ne'`
`pow_lt_one_of_lt` 📖	mathematical	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLT` `Monoid.toPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`pow_succ'` `mul_lt_one_of_lt_of_le` `pow_le_one_of_le` `LT.lt.le`

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_nsmul` 📖	mathematical	`Monotone`	`Monotone` `AddMonoid.toNSMul`	—	`zero_nsmul` `monotone_const` `succ_nsmul` `add`
`pow_const` 📖	mathematical	`Monotone`	`Monotone` `Monoid.toPow`	—	`pow_zero` `monotone_const` `pow_succ` `mul'`

Right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nsmul_neg` 📖	mathematical	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLT` `AddMonoid.toNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`LT.lt.ne'` `succ_nsmul` `add_neg_of_nonpos_of_neg` `nsmul_nonpos` `LT.lt.le`
`nsmul_neg_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`not_le` `LT.lt.not_ge` `nsmul_nonneg` `addRightMono_of_addRightStrictMono` `nsmul_neg`
`nsmul_nonneg` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`Eq.ge` `zero_nsmul` `succ_nsmul` `add_nonneg`
`nsmul_nonpos` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `AddMonoid.toNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`nsmul_nonneg` `OrderDual.addRightMono`
`one_le_pow_of_le` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`Eq.ge` `pow_zero` `pow_succ` `one_le_mul`
`pow_le_one_of_le` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `Monoid.toPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`one_le_pow_of_le` `OrderDual.mulRightMono`
`pow_lt_one_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`not_le` `LT.lt.not_ge` `one_le_pow_of_le` `mulRightMono_of_mulRightStrictMono` `pow_lt_one_of_lt`
`pow_lt_one_of_lt` 📖	mathematical	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLT` `Monoid.toPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`LT.lt.ne'` `pow_succ` `mul_lt_one_of_le_of_lt` `pow_le_one_of_le` `LT.lt.le`

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_nsmul` 📖	mathematical	`StrictMono`	`StrictMono` `AddMonoid.toNSMul`	—	`one_nsmul` `succ_nsmul` `add`
`pow_const` 📖	mathematical	`StrictMono`	`StrictMono` `Monoid.toPow`	—	`pow_one` `pow_succ` `mul'`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono` 📖	mathematical	—	`IsAddTorsionFree`	—	`StrictMono.injective` `nsmul_right_strictMono`
`instIsMulTorsionFreeOfMulLeftStrictMonoOfMulRightStrictMono` 📖	mathematical	—	`IsMulTorsionFree`	—	`StrictMono.injective` `pow_left_strictMono`
`le_max_of_sq_le_mul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`min_self` `min_le_max_of_mul_le_mul` `Eq.trans_le` `pow_two`
`le_max_of_two_nsmul_le_add` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNSMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`le_sup_iff` `min_self` `min_le_max_of_add_le_add` `Eq.trans_le` `two_nsmul`
`le_of_nsmul_le_nsmul_right` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNSMul`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`nsmul_le_nsmul_iff_right`
`le_of_pow_le_pow_left'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`pow_le_pow_iff_left`
`le_pow_sup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax` `Monoid.toPow`	—	`sup_le` `pow_le_pow_left'` `le_sup_left` `le_sup_right`
`le_self_nsmul` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `AddMonoid.toNSMul`	—	`one_nsmul` `nsmul_le_nsmul_left`
`le_self_pow` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `Monoid.toPow`	—	`pow_one` `pow_le_pow_right'`
`lt_max_of_sq_lt_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`min_self` `min_lt_max_of_mul_lt_mul` `Eq.trans_lt` `pow_two`
`lt_max_of_two_nsmul_lt_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNSMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`lt_sup_iff` `min_self` `min_lt_max_of_add_lt_add` `Eq.trans_lt` `two_nsmul`
`lt_of_nsmul_lt_nsmul_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNSMul`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Monotone.reflect_lt` `nsmul_right_mono`
`lt_of_pow_lt_pow_left'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Monotone.reflect_lt` `pow_left_mono`
`min_le_of_add_le_two_nsmul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin`	—	`inf_le_iff` `max_self` `min_le_max_of_add_le_add` `LE.le.trans_eq` `two_nsmul`
`min_le_of_mul_le_sq` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin`	—	`max_self` `min_le_max_of_mul_le_mul` `LE.le.trans_eq` `pow_two`
`min_lt_of_add_lt_two_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin`	—	`inf_lt_iff` `max_self` `min_lt_max_of_add_lt_add` `LT.lt.trans_eq` `two_nsmul`
`min_lt_of_mul_lt_sq` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin`	—	`max_self` `min_lt_max_of_mul_lt_mul` `LT.lt.trans_eq` `pow_two`
`nsmul_le_nsmul` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `AddMonoid.toNSMul`	—	`LE.le.trans` `nsmul_le_nsmul_right` `nsmul_le_nsmul_left`
`nsmul_le_nsmul_add_of_sq_le_add` 📖	mathematical	`Preorder.toLE` `AddMonoid.toNSMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `AddMonoid.toNSMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`one_nsmul` `zero_nsmul` `zero_add` `instReflLe` `succ_nsmul` `le_imp_le_of_le_of_le` `add_le_add_left` `le_refl` `add_assoc` `two_nsmul` `add_le_add_right`
`nsmul_le_nsmul_iff_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNSMul`	—	`StrictMono.le_iff_le` `nsmul_left_strictMono`
`nsmul_le_nsmul_iff_right` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNSMul`	—	`StrictMono.le_iff_le` `nsmul_right_strictMono`
`nsmul_le_nsmul_left` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `AddMonoid.toNSMul`	—	`nsmul_left_monotone`
`nsmul_le_nsmul_left_of_nonpos` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `AddMonoid.toNSMul`	—	`nsmul_le_nsmul_left` `OrderDual.addLeftMono`
`nsmul_le_nsmul_right` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE` `AddMonoid.toNSMul`	—	`zero_nsmul` `instReflLe` `succ_nsmul` `add_le_add`
`nsmul_left_monotone` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Monotone` `Nat.instPreorder` `AddMonoid.toNSMul`	—	`monotone_nat_of_le_succ` `succ_nsmul` `le_add_of_nonneg_right`
`nsmul_left_strictMono` 📖	mathematical	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`StrictMono` `Nat.instPreorder` `AddMonoid.toNSMul`	—	`strictMono_nat_of_lt_succ` `succ_nsmul` `lt_add_of_pos_right`
`nsmul_lt_nsmul_iff_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNSMul`	—	`StrictMono.lt_iff_lt` `nsmul_left_strictMono`
`nsmul_lt_nsmul_left` 📖	mathematical	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLT` `AddMonoid.toNSMul`	—	`nsmul_left_strictMono`
`nsmul_lt_nsmul_right` 📖	mathematical	`Preorder.toLT`	`Preorder.toLT` `AddMonoid.toNSMul`	—	`nsmul_right_strictMono`
`nsmul_neg` 📖	mathematical	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLT` `AddMonoid.toNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Left.nsmul_neg`
`nsmul_neg_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`lt_iff_lt_of_le_iff_le` `nsmul_nonneg_iff`
`nsmul_nonneg` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`Left.nsmul_nonneg`
`nsmul_nonneg_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`le_imp_le_of_lt_imp_lt` `nsmul_neg` `nsmul_nonneg`
`nsmul_nonpos` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLE` `AddMonoid.toNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Left.nsmul_nonpos`
`nsmul_nonpos_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`nsmul_nonneg_iff` `OrderDual.addLeftMono`
`nsmul_pos` 📖	mathematical	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`nsmul_neg` `OrderDual.addLeftMono`
`nsmul_pos_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`lt_iff_lt_of_le_iff_le` `nsmul_nonpos_iff`
`nsmul_right_mono` 📖	mathematical	—	`Monotone` `AddMonoid.toNSMul`	—	`Monotone.const_nsmul` `monotone_id`
`nsmul_right_strictMono` 📖	mathematical	—	`StrictMono` `AddMonoid.toNSMul`	—	`StrictMono.const_nsmul` `strictMono_id`
`one_le_pow_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`le_imp_le_of_lt_imp_lt` `pow_lt_one'` `one_le_pow_of_one_le'`
`one_le_pow_of_one_le'` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`Left.one_le_pow_of_le`
`one_le_zpow` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivInvMonoid.toZPow`	—	`CanLift.prf` `instCanLiftIntNatCastLeOfNat` `zpow_natCast` `one_le_pow_of_one_le'`
`one_lt_pow'` 📖	mathematical	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`pow_lt_one'` `OrderDual.mulLeftMono`
`one_lt_pow_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`lt_iff_lt_of_le_iff_le` `pow_le_one_iff`
`one_lt_zpow` 📖	mathematical	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivInvMonoid.toZPow`	—	`CanLift.prf` `instCanLiftIntNatCastLeOfNat` `zpow_natCast` `one_lt_pow'` `LT.lt.ne'`
`pow_inf_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Monoid.toPow` `SemilatticeInf.toMin`	—	`le_inf` `pow_le_pow_left'` `inf_le_left` `inf_le_right`
`pow_le_one'` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `Monoid.toPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`Left.pow_le_one_of_le`
`pow_le_one_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`one_le_pow_iff` `OrderDual.mulLeftMono`
`pow_le_pow` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `Monoid.toPow`	—	`LE.le.trans` `pow_le_pow_left'` `pow_le_pow_right'`
`pow_le_pow_iff_left` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow`	—	`StrictMono.le_iff_le` `pow_left_strictMono`
`pow_le_pow_iff_right'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow`	—	`StrictMono.le_iff_le` `pow_right_strictMono'`
`pow_le_pow_left'` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE` `Monoid.toPow`	—	`pow_zero` `instReflLe` `pow_succ` `mul_le_mul'`
`pow_le_pow_mul_of_sq_le_mul` 📖	mathematical	`Preorder.toLE` `Monoid.toPow` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `Monoid.toPow` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`pow_one` `pow_zero` `one_mul` `instReflLe` `pow_succ` `le_imp_le_of_le_of_le` `mul_le_mul_left` `le_refl` `mul_assoc` `sq` `mul_le_mul_right`
`pow_le_pow_right'` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `Monoid.toPow`	—	`pow_right_monotone`
`pow_le_pow_right_of_le_one'` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLE` `Monoid.toPow`	—	`pow_le_pow_right'` `OrderDual.mulLeftMono`
`pow_left_mono` 📖	mathematical	—	`Monotone` `Monoid.toPow`	—	`Monotone.pow_const` `monotone_id`
`pow_left_strictMono` 📖	mathematical	—	`StrictMono` `Monoid.toPow`	—	`StrictMono.pow_const` `strictMono_id`
`pow_lt_one'` 📖	mathematical	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLT` `Monoid.toPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`Left.pow_lt_one_of_lt`
`pow_lt_one_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`lt_iff_lt_of_le_iff_le` `one_le_pow_iff`
`pow_lt_pow_iff_right'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toPow`	—	`StrictMono.lt_iff_lt` `pow_right_strictMono'`
`pow_lt_pow_left'` 📖	mathematical	`Preorder.toLT`	`Preorder.toLT` `Monoid.toPow`	—	`pow_left_strictMono`
`pow_lt_pow_right'` 📖	mathematical	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Preorder.toLT` `Monoid.toPow`	—	`pow_right_strictMono'`
`pow_right_monotone` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monotone` `Nat.instPreorder` `Monoid.toPow`	—	`monotone_nat_of_le_succ` `pow_succ` `le_mul_of_one_le_right'`
`pow_right_strictMono'` 📖	mathematical	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`StrictMono` `Nat.instPreorder` `Monoid.toPow`	—	`strictMono_nat_of_lt_succ` `pow_succ` `lt_mul_of_one_lt_right'`
`zsmul_nonneg` 📖	mathematical	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubNegMonoid.toZSMul`	—	`CanLift.prf` `instCanLiftIntNatCastLeOfNat` `natCast_zsmul` `nsmul_nonneg`
`zsmul_pos` 📖	mathematical	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubNegMonoid.toZSMul`	—	`CanLift.prf` `instCanLiftIntNatCastLeOfNat` `natCast_zsmul` `nsmul_pos` `LT.lt.ne'`

---

← Back to Index