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	AddMonoid.toNatSMul	—	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.toNatSMul 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	AddMonoid.toNatSMul	—	zero_nsmul le_refl succ_nsmul add_nonneg
nsmul_nonpos 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	AddMonoid.toNatSMul	—	nsmul_nonneg OrderDual.addLeftMono
one_le_pow_of_le 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Monoid.toNatPow	—	pow_zero pow_succ one_le_mul
pow_le_one_of_le 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Monoid.toNatPow	—	one_le_pow_of_le OrderDual.mulLeftMono
pow_lt_one_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Monoid.toNatPow 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.toNatPow 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	Monoid.toNatPow	—	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	AddMonoid.toNatSMul	—	zero_nsmul monotone_const succ_nsmul add
pow_const 📖	mathematical	Monotone	Monoid.toNatPow	—	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	AddMonoid.toNatSMul	—	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.toNatSMul 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	AddMonoid.toNatSMul	—	Eq.ge zero_nsmul succ_nsmul add_nonneg
nsmul_nonpos 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	AddMonoid.toNatSMul	—	nsmul_nonneg OrderDual.addRightMono
one_le_pow_of_le 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Monoid.toNatPow	—	Eq.ge pow_zero pow_succ one_le_mul
pow_le_one_of_le 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Monoid.toNatPow	—	one_le_pow_of_le OrderDual.mulRightMono
pow_lt_one_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Monoid.toNatPow 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	Monoid.toNatPow	—	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	AddMonoid.toNatSMul	—	one_nsmul succ_nsmul add
pow_const 📖	mathematical	StrictMono	Monoid.toNatPow	—	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.toNatPow MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	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.toNatSMul AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	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 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoid.toNatSMul	—	—	nsmul_le_nsmul_iff_right
le_of_pow_le_pow_left' 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Monoid.toNatPow	—	—	pow_le_pow_iff_left
le_pow_sup 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder SemilatticeSup.toMax Monoid.toNatPow	—	sup_le pow_le_pow_left' le_sup_left le_sup_right
le_self_nsmul 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	AddMonoid.toNatSMul	—	one_nsmul nsmul_le_nsmul_left
le_self_pow 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Monoid.toNatPow	—	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.toNatPow MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	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.toNatSMul AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	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 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoid.toNatSMul	—	—	Monotone.reflect_lt nsmul_right_mono
lt_of_pow_lt_pow_left' 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Monoid.toNatPow	—	—	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.toNatSMul	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.toNatPow	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.toNatSMul	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.toNatPow	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	AddMonoid.toNatSMul	—	LE.le.trans nsmul_le_nsmul_right nsmul_le_nsmul_left
nsmul_le_nsmul_add_of_sq_le_add 📖	—	Preorder.toLE AddMonoid.toNatSMul AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—	one_nsmul zero_nsmul zero_add le_refl succ_nsmul le_imp_le_of_le_of_le add_le_add_left 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 AddMonoid.toNatSMul	—	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.toNatSMul	—	StrictMono.le_iff_le nsmul_right_strictMono
nsmul_le_nsmul_left 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	AddMonoid.toNatSMul	—	nsmul_left_monotone
nsmul_le_nsmul_left_of_nonpos 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	AddMonoid.toNatSMul	—	nsmul_le_nsmul_left OrderDual.addLeftMono
nsmul_le_nsmul_right 📖	mathematical	Preorder.toLE	AddMonoid.toNatSMul	—	zero_nsmul le_refl succ_nsmul add_le_add
nsmul_left_monotone 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	Monotone Nat.instPreorder AddMonoid.toNatSMul	—	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.toNatSMul	—	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	AddMonoid.toNatSMul	—	StrictMono.lt_iff_lt nsmul_left_strictMono
nsmul_lt_nsmul_left 📖	mathematical	Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	AddMonoid.toNatSMul	—	nsmul_left_strictMono
nsmul_lt_nsmul_right 📖	mathematical	Preorder.toLT	AddMonoid.toNatSMul	—	nsmul_right_strictMono
nsmul_neg 📖	mathematical	Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	AddMonoid.toNatSMul	—	Left.nsmul_neg
nsmul_neg_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoid.toNatSMul 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	AddMonoid.toNatSMul	—	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.toNatSMul	—	le_imp_le_of_lt_imp_lt nsmul_neg nsmul_nonneg
nsmul_nonpos 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	AddMonoid.toNatSMul	—	Left.nsmul_nonpos
nsmul_nonpos_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoid.toNatSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	nsmul_nonneg_iff OrderDual.addLeftMono
nsmul_pos 📖	mathematical	Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	AddMonoid.toNatSMul	—	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.toNatSMul	—	lt_iff_lt_of_le_iff_le nsmul_nonpos_iff
nsmul_right_mono 📖	mathematical	—	Monotone AddMonoid.toNatSMul	—	Monotone.const_nsmul monotone_id
nsmul_right_strictMono 📖	mathematical	—	StrictMono AddMonoid.toNatSMul	—	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.toNatPow	—	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	Monoid.toNatPow	—	Left.one_le_pow_of_le
one_le_zpow 📖	mathematical	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	Monoid.toNatPow	—	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.toNatPow	—	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	DivInvMonoid.toZPow	—	CanLift.prf instCanLiftIntNatCastLeOfNat zpow_natCast one_lt_pow' LT.lt.ne'
pow_inf_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Monoid.toNatPow 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	Monoid.toNatPow	—	Left.pow_le_one_of_le
pow_le_one_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Monoid.toNatPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	one_le_pow_iff OrderDual.mulLeftMono
pow_le_pow 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Monoid.toNatPow	—	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.toNatPow	—	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 Monoid.toNatPow	—	StrictMono.le_iff_le pow_right_strictMono'
pow_le_pow_left' 📖	mathematical	Preorder.toLE	Monoid.toNatPow	—	pow_zero pow_succ mul_le_mul'
pow_le_pow_mul_of_sq_le_mul 📖	—	Preorder.toLE Monoid.toNatPow MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—	pow_one pow_zero one_mul 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	Monoid.toNatPow	—	pow_right_monotone
pow_le_pow_right_of_le_one' 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Monoid.toNatPow	—	pow_le_pow_right' OrderDual.mulLeftMono
pow_left_mono 📖	mathematical	—	Monotone Monoid.toNatPow	—	Monotone.pow_const monotone_id
pow_left_strictMono 📖	mathematical	—	StrictMono Monoid.toNatPow	—	StrictMono.pow_const strictMono_id
pow_lt_one' 📖	mathematical	Preorder.toLT MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Monoid.toNatPow	—	Left.pow_lt_one_of_lt
pow_lt_one_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Monoid.toNatPow 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	Monoid.toNatPow	—	StrictMono.lt_iff_lt pow_right_strictMono'
pow_lt_pow_left' 📖	mathematical	Preorder.toLT	Monoid.toNatPow	—	pow_left_strictMono
pow_lt_pow_right' 📖	mathematical	Preorder.toLT MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Monoid.toNatPow	—	pow_right_strictMono'
pow_right_monotone 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Monotone Nat.instPreorder Monoid.toNatPow	—	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.toNatPow	—	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	SubNegMonoid.toZSMul	—	CanLift.prf instCanLiftIntNatCastLeOfNat natCast_zsmul nsmul_nonneg
zsmul_pos 📖	mathematical	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