Log

📁 Source: Mathlib/Data/Int/Log.lean

Statistics

Metric	Count
Definitions clog, clogZPowGi, zpowLogGi	3
Theorems clog_inv, clog_mono_right, clog_natCast, clog_ofNat, clog_of_left_le_one, clog_of_one_le_right, clog_of_right_le_one, clog_of_right_le_zero, clog_one_left, clog_one_right, clog_zero_left, clog_zero_right, clog_zpow, le_zpow_iff_clog_le, log_inv, log_mono_right, log_natCast, log_ofNat, log_of_left_le_one, log_of_one_le_right, log_of_right_le_one, log_of_right_le_zero, log_one_left, log_one_right, log_zero_left, log_zero_right, log_zpow, lt_zpow_iff_log_lt, lt_zpow_succ_log_self, neg_clog_inv_eq_log, neg_log_inv_eq_clog, self_le_zpow_clog, zpow_le_iff_le_log, zpow_log_le_self, zpow_lt_iff_lt_clog, zpow_pred_clog_lt_self	36
Total	39

Int

Definitions

Name	Category	Theorems
clog 📖	CompOp	21 math math: log_inv, self_le_zpow_clog, clog_mono_right, clog_of_right_le_one, clog_one_left, zpow_pred_clog_lt_self, clog_zero_left, clog_of_left_le_one, clog_of_right_le_zero, clog_of_one_le_right, clog_zpow, Real.ceil_logb_natCast, le_zpow_iff_clog_le, clog_natCast, clog_one_right, zpow_lt_iff_lt_clog, neg_log_inv_eq_clog, clog_ofNat, neg_clog_inv_eq_log, clog_inv, clog_zero_right
clogZPowGi 📖	CompOp	—
zpowLogGi 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
clog_inv 📖	mathematical	—	clog InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero log	—	lt_or_ge le_total clog_of_right_le_one inv_le_one_of_one_le₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass log_of_one_le_right inv_inv clog_of_one_le_right one_le_inv₀ log_of_right_le_one neg_neg clog_of_right_le_zero inv_nonpos IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing log_of_right_le_zero neg_zero
clog_mono_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Preorder.toLE	clog	—	lt_of_lt_of_le neg_log_inv_eq_clog neg_le_neg_iff instAddLeftMono covariant_swap_add_of_covariant_add log_mono_right inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono inv_le_inv₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono
clog_natCast 📖	mathematical	—	clog AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Nat.clog	—	Nat.cast_zero clog_of_right_le_one IsStrictOrderedRing.toZeroLEOneClass inv_zero Nat.floor_zero Nat.log_zero_right neg_zero Nat.clog_zero_right clog_of_one_le_right Nat.cast_add Nat.cast_one covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.ceil_eq_iff add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsCancelAdd.toIsLeftCancelAdd NeZero.charZero_one IsStrictOrderedRing.toCharZero
clog_ofNat 📖	mathematical	—	clog Nat.clog	—	clog_natCast
clog_of_left_le_one 📖	mathematical	—	clog	—	neg_log_inv_eq_clog log_of_left_le_one neg_zero
clog_of_one_le_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	clog Nat.clog Nat.ceil	—	—
clog_of_right_le_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	clog Nat.log Nat.floor InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	LE.le.eq_or_lt clog.eq_1 inv_one Nat.ceil_one Nat.floor_one Nat.log_one_right Nat.clog_one_right neg_zero LT.lt.not_ge
clog_of_right_le_zero 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	clog	—	clog.eq_1 LT.lt.not_ge LE.le.trans_lt zero_lt_one IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero neg_eq_zero Nat.log_eq_zero_iff le_or_gt lt_of_le_of_lt Nat.floor_le_one_of_le_one LE.le.trans inv_nonpos IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing zero_le_one
clog_one_left 📖	mathematical	—	clog	—	Nat.clog_one_left Nat.cast_zero Nat.log_one_left neg_zero
clog_one_right 📖	mathematical	—	clog AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	clog_of_one_le_right le_rfl Nat.ceil_one Nat.clog_one_right
clog_zero_left 📖	mathematical	—	clog	—	Nat.clog_zero_left Nat.cast_zero Nat.log_zero_left neg_zero
clog_zero_right 📖	mathematical	—	clog MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	clog_of_right_le_zero le_rfl
clog_zpow 📖	mathematical	—	clog DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring	—	neg_log_inv_eq_clog zpow_neg log_zpow neg_neg
le_zpow_iff_clog_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	Preorder.toLE DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne clog	—	zpow_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toCharZero LT.lt.trans zero_lt_one Nat.instZeroLEOneClass GaloisConnection.le_iff_le GaloisInsertion.gc
log_inv 📖	mathematical	—	log InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero clog	—	inv_inv clog_inv neg_neg
log_mono_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Preorder.toLE	log	—	le_total lt_of_lt_of_le log_of_right_le_one neg_le_neg_iff instAddLeftMono covariant_swap_add_of_covariant_add Nat.cast_le instZeroLEOneClass instCharZero Nat.clog_mono_right Nat.ceil_mono inv_le_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono log_of_one_le_right LE.le.trans neg_nonpos le_refl le_antisymm Nat.log_mono_right Nat.floor_mono
log_natCast 📖	mathematical	—	log AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Nat.log	—	Nat.cast_zero log_of_right_le_one IsStrictOrderedRing.toZeroLEOneClass inv_zero Nat.ceil_zero Nat.clog_zero_right neg_zero Nat.log_zero_right log_of_one_le_right Nat.cast_add Nat.cast_one covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.floor_natCast
log_ofNat 📖	mathematical	—	log Nat.log	—	log_natCast
log_of_left_le_one 📖	mathematical	—	log	—	le_total log_of_one_le_right Nat.log_of_left_le_one log_of_right_le_one Nat.clog_of_left_le_one neg_zero
log_of_one_le_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	log Nat.log Nat.floor	—	—
log_of_right_le_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	log Nat.clog Nat.ceil InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	LE.le.eq_or_lt log.eq_1 inv_one Nat.ceil_one Nat.floor_one Nat.log_one_right Nat.clog_one_right neg_zero LT.lt.not_ge
log_of_right_le_zero 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	log	—	log_of_right_le_one LE.le.trans zero_le_one IsStrictOrderedRing.toZeroLEOneClass Nat.clog_of_right_le_one Eq.trans_le Nat.ceil_eq_zero inv_nonpos IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instZeroLEOneClass neg_zero
log_one_left 📖	mathematical	—	log	—	Nat.log_one_left Nat.cast_zero Nat.clog_one_left neg_zero
log_one_right 📖	mathematical	—	log AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	log_of_one_le_right le_rfl Nat.floor_one Nat.log_one_right
log_zero_left 📖	mathematical	—	log	—	Nat.log_zero_left Nat.cast_zero Nat.clog_zero_left neg_zero
log_zero_right 📖	mathematical	—	log MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	log_of_right_le_zero le_rfl
log_zpow 📖	mathematical	—	log DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring	—	log_of_one_le_right one_le_zpow₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass Nat.cast_one IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toCharZero LT.lt.le zpow_natCast Nat.cast_pow Nat.floor_natCast Nat.log_pow log_of_right_le_one zpow_le_one_of_nonpos₀ neg_nonpos instAddLeftMono zpow_neg inv_inv Nat.ceil_natCast Nat.clog_pow
lt_zpow_iff_log_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne log	—	GaloisConnection.lt_iff_lt zpow_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toCharZero LT.lt.trans zero_lt_one Nat.instZeroLEOneClass GaloisCoinsertion.gc
lt_zpow_succ_log_self 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring log	—	le_or_gt log_of_right_le_zero zero_add zpow_one LE.le.trans_lt LT.lt.trans_le zero_lt_one IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Nat.cast_one IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing LT.lt.le log_of_one_le_right zpow_natCast Nat.cast_pow Nat.lt_of_floor_lt Nat.lt_pow_succ_log_self log_of_right_le_one one_lt_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.clog_pos Nat.one_lt_cast Nat.le_ceil neg_add_eq_sub neg_sub zpow_neg lt_inv_comm₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono pow_pos Nat.cast_pos instNontrivialOfCharZero LT.lt.trans Nat.instZeroLEOneClass Nat.lt_ceil Nat.pow_pred_clog_lt_self
neg_clog_inv_eq_log 📖	mathematical	—	clog InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero log	—	clog_inv neg_neg
neg_log_inv_eq_clog 📖	mathematical	—	log InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero clog	—	log_inv neg_neg
self_le_zpow_clog 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring clog	—	le_or_gt clog_of_right_le_zero zpow_zero LE.le.trans zero_le_one IsStrictOrderedRing.toZeroLEOneClass neg_log_inv_eq_clog zpow_neg le_inv_comm₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono zpow_pos Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero LE.le.trans_lt Nat.instZeroLEOneClass zpow_log_le_self inv_pos
zpow_le_iff_le_log 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	Preorder.toLE DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne log	—	GaloisConnection.le_iff_le zpow_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toCharZero LT.lt.trans zero_lt_one Nat.instZeroLEOneClass GaloisCoinsertion.gc
zpow_log_le_self 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	Preorder.toLE DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne log	—	le_total log_of_one_le_right zpow_natCast Nat.cast_pow Nat.le_floor_iff LT.lt.le Nat.pow_log_le_self LT.lt.ne' Nat.floor_pos log_of_right_le_one zpow_neg inv_le_of_inv_le₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.ceil_le Nat.le_pow_clog
zpow_lt_iff_lt_clog 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne clog	—	zpow_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toCharZero LT.lt.trans zero_lt_one Nat.instZeroLEOneClass GaloisConnection.lt_iff_lt GaloisInsertion.gc
zpow_pred_clog_lt_self 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne clog	—	neg_log_inv_eq_clog neg_add' zpow_neg inv_lt_comm₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono zpow_pos IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero LE.le.trans_lt zero_le_one Nat.instZeroLEOneClass lt_zpow_succ_log_self

---

← Back to Index