Base

📁 Source: Mathlib/Analysis/SpecialFunctions/Log/Base.lean

Statistics

Metric	Count
Definitions `logb`	1
Theorems `logb`, `logb`, `logb`, `logb`, `logb`, `logb_prod`, `ceil_logb_natCast`, `continuousAt_logb`, `continuousAt_logb_iff`, `continuousOn_logb`, `continuous_logb`, `continuous_logb'`, `div_logb`, `eq_one_of_pos_of_logb_eq_zero`, `eq_one_of_pos_of_logb_eq_zero_of_base_lt_one`, `floor_logb_natCast`, `induction_Ico_mul`, `inv_logb`, `inv_logb_div_base`, `inv_logb_mul_base`, `isBigO_log_const_mul_log_atTop`, `isBigO_log_mul_const_log_atTop`, `isBigO_logb_const_mul_log_atTop`, `isBigO_logb_log`, `isBigO_logb_mul_const_log_atTop`, `isLittleO_const_logb_atTop`, `isLittleO_logb_id_atTop`, `isLittleO_pow_logb_id_atTop`, `le_logb_iff_rpow_le`, `le_logb_iff_rpow_le_of_base_lt_one`, `log2_le_logb`, `log_div_log`, `logb_abs`, `logb_abs_base`, `logb_div`, `logb_div_base`, `logb_eq_iff_rpow_eq`, `logb_eq_zero`, `logb_injOn_pos`, `logb_injOn_pos_of_base_lt_one`, `logb_inv`, `logb_inv_base`, `logb_le_iff_le_rpow`, `logb_le_iff_le_rpow_of_base_lt_one`, `logb_le_logb`, `logb_le_logb_of_base_lt_one`, `logb_le_logb_of_le`, `logb_lt_iff_lt_rpow`, `logb_lt_iff_lt_rpow_of_base_lt_one`, `logb_lt_logb`, `logb_lt_logb_iff`, `logb_lt_logb_iff_of_base_lt_one`, `logb_lt_logb_of_base_lt_one`, `logb_mul`, `logb_mul_base`, `logb_nat_eq_sum_factorization`, `logb_ne_zero_of_pos_of_ne_one`, `logb_ne_zero_of_pos_of_ne_one_of_base_lt_one`, `logb_neg`, `logb_neg_base_eq_logb`, `logb_neg_eq_logb`, `logb_neg_iff`, `logb_neg_iff_of_base_lt_one`, `logb_neg_of_base_lt_one`, `logb_nonneg`, `logb_nonneg_iff`, `logb_nonneg_iff_of_base_lt_one`, `logb_nonneg_of_base_lt_one`, `logb_nonpos`, `logb_nonpos_iff`, `logb_nonpos_iff'`, `logb_nonpos_iff_of_base_lt_one`, `logb_one`, `logb_one_left`, `logb_one_left_eq_zero`, `logb_pos`, `logb_pos_iff`, `logb_pos_iff_of_base_lt_one`, `logb_pos_of_base_lt_one`, `logb_pow`, `logb_prod`, `logb_rpow`, `logb_rpow_eq_mul_logb_of_pos`, `logb_self_eq_one`, `logb_self_eq_one_iff`, `logb_surjective`, `logb_zero`, `logb_zero_left`, `logb_zero_left_eq_zero`, `lt_logb_iff_rpow_lt`, `lt_logb_iff_rpow_lt_of_base_lt_one`, `mul_logb`, `natCeil_logb_natCast`, `natFloor_logb_natCast`, `natLog_le_logb`, `range_logb`, `rpow_logb`, `rpow_logb_eq_abs`, `rpow_logb_of_neg`, `strictAntiOn_logb`, `strictAntiOn_logb_of_base_lt_one`, `strictMonoOn_logb`, `strictMonoOn_logb_of_base_lt_one`, `surjOn_logb`, `surjOn_logb'`, `tendsto_abs_logb_atTop`, `tendsto_logb_atTop`, `tendsto_logb_atTop_of_base_lt_one`, `tendsto_logb_comp_add_sub_logb`, `tendsto_logb_nat_add_one_sub_logb`, `tendsto_logb_nhdsGT_zero`, `tendsto_logb_nhdsGT_zero_of_base_lt_one`, `tendsto_logb_nhdsNE_zero`, `tendsto_logb_nhdsNE_zero_of_base_lt_one`, `tendsto_pow_logb_div_mul_add_atTop`	115
Total	116

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`logb` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.logb`	—	`ContinuousOn.comp_continuous` `Real.continuousOn_logb`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`logb` 📖	mathematical	`ContinuousAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.logb`	—	`Filter.Tendsto.logb`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`logb` 📖	mathematical	`ContinuousOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.logb`	—	`ContinuousWithinAt.logb`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`logb` 📖	mathematical	`ContinuousWithinAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.logb`	—	`Filter.Tendsto.logb`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`logb` 📖	mathematical	`Filter.Tendsto` `Real` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.logb`	—	`comp` `ContinuousAt.tendsto` `Real.continuousAt_logb`

Finsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`logb_prod` 📖	mathematical	`DFunLike.coe` `Finsupp` `instFunLike`	`Real.logb` `prod` `Real` `Real.instCommMonoid` `sum` `Real.instAddCommMonoid`	—	`Real.logb_prod` `mem_support_iff`

Real

Definitions

Name	Category	Theorems
`logb` 📖	CompOp	109 math math: `Continuous.logb`, `Filter.Tendsto.logb`, `logb_zero_left`, `isLittleO_logb_id_atTop`, `logb_le_iff_le_rpow`, `logb_neg_of_base_lt_one`, `logb_one`, `log2_le_logb`, `strictAntiOn_logb`, `logb_le_logb_of_base_lt_one`, `natFloor_logb_natCast`, `logb_le_iff_le_rpow_of_base_lt_one`, `logb_inv`, `log_div_log`, `logb_mul`, `inv_logb_div_base`, `le_logb_iff_rpow_le`, `logb_lt_iff_lt_rpow`, `logb_eq_zero`, `range_logb`, `logb_eq_iff_rpow_eq`, `Finsupp.logb_prod`, `logb_surjective`, `ContinuousOn.logb`, `logb_prod`, `logb_neg_base_eq_logb`, `logb_zero_left_eq_zero`, `surjOn_logb'`, `logb_div`, `logb_rpow_eq_mul_logb_of_pos`, `logb_abs_base`, `strictMonoOn_logb_of_base_lt_one`, `logb_self_eq_one`, `ContinuousAt.logb`, `logb_nat_eq_sum_factorization`, `logb_pos_of_base_lt_one`, `logb_lt_logb_of_base_lt_one`, `natCeil_logb_natCast`, `logb_pow`, `logb_neg_iff_of_base_lt_one`, `logb_self_eq_one_iff`, `continuousOn_logb`, `continuousAt_logb_iff`, `isBigO_logb_mul_const_log_atTop`, `logb_injOn_pos`, `rpow_logb_eq_abs`, `logb_nonneg_of_base_lt_one`, `logb_nonpos_iff_of_base_lt_one`, `logb_lt_logb_iff_of_base_lt_one`, `isBigO_logb_log`, `logb_lt_logb_iff`, `continuous_logb`, `logb_lt_iff_lt_rpow_of_base_lt_one`, `continuous_logb'`, `mul_logb`, `tendsto_logb_atTop`, `rpow_logb`, `logb_one_left`, `strictMonoOn_logb`, `logb_one_left_eq_zero`, `logb_nonpos_iff'`, `lt_logb_iff_rpow_lt`, `tendsto_logb_nhdsNE_zero_of_base_lt_one`, `logb_inv_base`, `inv_logb_mul_base`, `logb_le_logb_of_le`, `natLog_le_logb`, `rpow_logb_of_neg`, `strictAntiOn_logb_of_base_lt_one`, `tendsto_logb_atTop_of_base_lt_one`, `logb_nonneg_iff_of_base_lt_one`, `ContinuousWithinAt.logb`, `logb_injOn_pos_of_base_lt_one`, `ceil_logb_natCast`, `tendsto_logb_comp_add_sub_logb`, `logb_nonpos`, `surjOn_logb`, `logb_le_logb`, `floor_logb_natCast`, `logb_mul_base`, `logb_abs`, `logb_pos_iff_of_base_lt_one`, `logb_div_base`, `tendsto_abs_logb_atTop`, `tendsto_pow_logb_div_mul_add_atTop`, `logb_zero`, `tendsto_logb_nhdsGT_zero_of_base_lt_one`, `logb_nonpos_iff`, `continuousAt_logb`, `logb_lt_logb`, `logb_pos`, `logb_neg`, `isBigO_logb_const_mul_log_atTop`, `lt_logb_iff_rpow_lt_of_base_lt_one`, `div_logb`, `le_logb_iff_rpow_le_of_base_lt_one`, `logb_neg_iff`, `logb_neg_eq_logb`, `logb_nonneg_iff`, `isLittleO_const_logb_atTop`, `tendsto_logb_nhdsGT_zero`, `logb_rpow`, `isLittleO_pow_logb_id_atTop`, `inv_logb`, `tendsto_logb_nhdsNE_zero`, `logb_pos_iff`, `logb_nonneg`, `Rat.AbsoluteValue.le_pow_log`, `tendsto_logb_nat_add_one_sub_logb`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ceil_logb_natCast` 📖	mathematical	`Real` `instLE` `instZero`	`Int.ceil` `instRing` `linearOrder` `instFloorRing` `logb` `instNatCast` `Int.clog` `Field.toSemifield` `instField` `FloorRing.toFloorSemiring` `instIsStrictOrderedRing`	—	`instIsStrictOrderedRing` `LE.le.eq_or_lt` `logb_zero` `Int.clog_zero_right` `Int.ceil_zero` `Nat.one_lt_cast` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instZeroLEOneClass` `RCLike.charZero_rclike` `le_antisymm` `Int.ceil_le` `logb_le_iff_le_rpow` `rpow_intCast` `Int.self_le_zpow_clog` `Int.le_zpow_iff_clog_le` `Eq.trans_le` `rpow_logb` `LT.lt.trans` `zero_lt_one` `NeZero.charZero_one` `LT.lt.ne'` `rpow_le_rpow_of_exponent_le` `LT.lt.le` `Int.le_ceil` `or_iff_not_and_not` `CharP.cast_eq_zero` `CharP.ofCharZero` `logb_zero_left` `Int.clog_zero_left` `Nat.cast_one` `logb_one_left` `Int.clog_one_left`
`continuousAt_logb` 📖	mathematical	—	`ContinuousAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `logb`	—	`ContinuousAt.div_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuousAt_log`
`continuousAt_logb_iff` 📖	mathematical	`Real` `instLT` `instZero`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `logb`	—	`lt_or_gt_of_ne` `not_tendsto_nhds_of_tendsto_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `instIsOrderedRing` `instNontrivial` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `punctured_nhds_module_neBot` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `tendsto_logb_nhdsNE_zero_of_base_lt_one` `Filter.Tendsto.mono_left` `ContinuousAt.tendsto` `inf_le_left` `not_tendsto_nhds_of_tendsto_atBot` `instNoBotOrderOfNoMinOrder` `instNoMinOrderOfNontrivial` `instClosedIicTopology` `tendsto_logb_nhdsNE_zero` `continuousAt_logb`
`continuousOn_logb` 📖	mathematical	—	`ContinuousOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `logb` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `instZero`	—	`ContinuousOn.div_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuousOn_log`
`continuous_logb` 📖	mathematical	—	`Continuous` `Real` `instZero` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `logb`	—	`Continuous.div_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_log`
`continuous_logb'` 📖	mathematical	—	`Continuous` `Real` `instLT` `instZero` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `logb`	—	`Continuous.div_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_log'`
`div_logb` 📖	mathematical	—	`Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `logb`	—	`div_div_div_cancel_left'` `log_ne_zero`
`eq_one_of_pos_of_logb_eq_zero` 📖	—	`Real` `instLT` `instOne` `instZero` `logb`	—	—	`logb_injOn_pos` `Set.mem_Ioi` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `logb_one`
`eq_one_of_pos_of_logb_eq_zero_of_base_lt_one` 📖	—	`Real` `instLT` `instZero` `instOne` `logb`	—	—	`logb_injOn_pos_of_base_lt_one` `Set.mem_Ioi` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `logb_one`
`floor_logb_natCast` 📖	mathematical	`Real` `instLE` `instZero`	`Int.floor` `instRing` `linearOrder` `instFloorRing` `logb` `instNatCast` `Int.log` `Field.toSemifield` `instField` `FloorRing.toFloorSemiring` `instIsStrictOrderedRing`	—	`instIsStrictOrderedRing` `LE.le.eq_or_lt` `logb_zero` `Int.log_zero_right` `Int.floor_zero` `Nat.one_lt_cast` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instZeroLEOneClass` `RCLike.charZero_rclike` `le_antisymm` `Int.zpow_le_iff_le_log` `rpow_intCast` `rpow_le_rpow_of_exponent_le` `LT.lt.le` `Int.floor_le` `rpow_logb` `LT.lt.trans` `zero_lt_one` `NeZero.charZero_one` `LT.lt.ne'` `Int.le_floor` `le_logb_iff_rpow_le` `Int.zpow_log_le_self` `or_iff_not_and_not` `CharP.cast_eq_zero` `CharP.ofCharZero` `logb_zero_left` `Int.log_zero_left` `Nat.cast_one` `logb_one_left` `Int.log_one_left`
`induction_Ico_mul` 📖	—	`Real` `instLT` `instOne` `instZero` `instLE`	—	—	`zero_add` `pow_one` `Set.Ico_subset_Ico_union_Ico` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `LT.lt.trans_le` `Set.mem_Ico` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `rpow_natCast` `logb_lt_iff_lt_rpow` `Nat.cast_add` `Nat.cast_one` `Nat.lt_floor_add_one`
`inv_logb` 📖	mathematical	—	`Real` `instInv` `logb`	—	`inv_div`
`inv_logb_div_base` 📖	mathematical	—	`Real` `instInv` `logb` `DivInvMonoid.toDiv` `instDivInvMonoid` `instSub`	—	`inv_logb` `logb_div`
`inv_logb_mul_base` 📖	mathematical	—	`Real` `instInv` `logb` `instMul` `instAdd`	—	`inv_logb` `logb_mul`
`isBigO_log_const_mul_log_atTop` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `norm` `Filter.atTop` `instPreorder` `log` `instMul`	—	`eq_or_ne` `MulZeroClass.zero_mul` `log_zero` `Asymptotics.IsLittleO.isBigO` `isLittleO_const_log_atTop` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `instIsOrderedRing` `instNontrivial` `Filter.univ_mem'` `log_mul` `LT.lt.ne'` `Asymptotics.IsBigO.add` `Asymptotics.isBigO_refl`
`isBigO_log_mul_const_log_atTop` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `norm` `Filter.atTop` `instPreorder` `log` `instMul`	—	`mul_comm` `isBigO_log_const_mul_log_atTop`
`isBigO_logb_const_mul_log_atTop` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `norm` `Filter.atTop` `instPreorder` `logb` `instMul` `log`	—	`div_eq_mul_inv` `mul_comm` `Asymptotics.IsBigO.const_mul_left` `isBigO_log_const_mul_log_atTop`
`isBigO_logb_log` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `norm` `Top.top` `Filter` `Filter.instTop` `logb` `log`	—	`logb_neg_base_eq_logb` `logb_one_left_eq_zero` `Asymptotics.isBigO_zero` `logb_zero_left_eq_zero` `div_eq_mul_inv` `mul_comm` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_inv` `Asymptotics.IsBigO.const_mul_left` `Asymptotics.isBigO_refl`
`isBigO_logb_mul_const_log_atTop` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `norm` `Filter.atTop` `instPreorder` `logb` `instMul` `log`	—	`mul_comm` `isBigO_logb_const_mul_log_atTop`
`isLittleO_const_logb_atTop` 📖	mathematical	—	`Asymptotics.IsLittleO` `Real` `norm` `Filter.atTop` `instPreorder` `logb`	—	`Asymptotics.isLittleO_const_left` `tendsto_abs_logb_atTop`
`isLittleO_logb_id_atTop` 📖	mathematical	—	`Asymptotics.IsLittleO` `Real` `norm` `Filter.atTop` `instPreorder` `logb`	—	`Asymptotics.IsLittleO.congr_left` `isLittleO_pow_logb_id_atTop` `pow_one`
`isLittleO_pow_logb_id_atTop` 📖	mathematical	—	`Asymptotics.IsLittleO` `Real` `norm` `Filter.atTop` `instPreorder` `Monoid.toNatPow` `instMonoid` `logb`	—	`Asymptotics.isLittleO_iff_tendsto'` `Filter.mp_mem` `Filter.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `instIsOrderedRing` `instNontrivial` `Filter.univ_mem'` `one_mul` `add_zero` `tendsto_pow_logb_div_mul_add_atTop` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike`
`le_logb_iff_rpow_le` 📖	mathematical	`Real` `instLT` `instOne` `instZero`	`instLE` `logb` `instPow`	—	`rpow_le_rpow_left_iff` `rpow_logb`
`le_logb_iff_rpow_le_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`instLE` `logb` `instPow`	—	`rpow_le_rpow_left_iff_of_base_lt_one` `rpow_logb`
`log2_le_logb` 📖	mathematical	—	`Real` `instLE` `instNatCast` `logb` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `RCLike.charZero_rclike` `Nat.log2_eq_log_two` `natLog_le_logb`
`log_div_log` 📖	mathematical	—	`Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `log` `logb`	—	—
`logb_abs` 📖	mathematical	—	`logb` `abs` `Real` `lattice` `instAddGroup`	—	`logb.eq_1` `log_abs`
`logb_abs_base` 📖	mathematical	—	`logb` `abs` `Real` `lattice` `instAddGroup`	—	`logb.eq_1` `log_abs`
`logb_div` 📖	mathematical	—	`logb` `Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `instSub`	—	`log_div` `sub_div`
`logb_div_base` 📖	mathematical	—	`logb` `Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `instInv` `instSub`	—	`inv_logb_div_base` `inv_inv`
`logb_eq_iff_rpow_eq` 📖	mathematical	`Real` `instLT` `instZero`	`logb` `instPow`	—	`rpow_logb` `logb_rpow`
`logb_eq_zero` 📖	mathematical	—	`logb` `Real` `instZero` `instOne` `instNeg`	—	—
`logb_injOn_pos` 📖	mathematical	`Real` `instLT` `instOne`	`Set.InjOn` `logb` `Set.Ioi` `instPreorder` `instZero`	—	`StrictMonoOn.injOn` `strictMonoOn_logb`
`logb_injOn_pos_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`Set.InjOn` `logb` `Set.Ioi` `instPreorder`	—	`StrictAntiOn.injOn` `strictAntiOn_logb_of_base_lt_one`
`logb_inv` 📖	mathematical	—	`logb` `Real` `instInv` `instNeg`	—	`log_inv` `neg_div`
`logb_inv_base` 📖	mathematical	—	`logb` `Real` `instInv` `instNeg`	—	`log_inv` `div_neg`
`logb_le_iff_le_rpow` 📖	mathematical	`Real` `instLT` `instOne` `instZero`	`instLE` `logb` `instPow`	—	`rpow_le_rpow_left_iff` `rpow_logb`
`logb_le_iff_le_rpow_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`instLE` `logb` `instPow`	—	`rpow_le_rpow_left_iff_of_base_lt_one` `rpow_logb`
`logb_le_logb` 📖	mathematical	`Real` `instLT` `instOne` `instZero`	`instLE` `logb`	—	`logb.eq_1` `div_le_div_iff_of_pos_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `instIsStrictOrderedRing` `log_pos` `log_le_log_iff`
`logb_le_logb_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`instLE` `logb`	—	`logb.eq_1` `div_le_div_right_of_neg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `log_neg` `log_le_log_iff`
`logb_le_logb_of_le` 📖	mathematical	`Real` `instLT` `instOne` `instZero` `instLE`	`logb`	—	`logb_le_logb` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le`
`logb_lt_iff_lt_rpow` 📖	mathematical	`Real` `instLT` `instOne` `instZero`	`logb` `instPow`	—	`rpow_lt_rpow_left_iff` `rpow_logb`
`logb_lt_iff_lt_rpow_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`logb` `instPow`	—	`rpow_lt_rpow_left_iff_of_base_lt_one` `rpow_logb`
`logb_lt_logb` 📖	mathematical	`Real` `instLT` `instOne` `instZero`	`logb`	—	`logb.eq_1` `div_lt_div_iff_of_pos_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `instIsStrictOrderedRing` `log_pos` `log_lt_log`
`logb_lt_logb_iff` 📖	mathematical	`Real` `instLT` `instOne` `instZero`	`logb`	—	`logb.eq_1` `div_lt_div_iff_of_pos_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `instIsStrictOrderedRing` `log_pos` `log_lt_log_iff`
`logb_lt_logb_iff_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`logb`	—	`logb.eq_1` `div_lt_div_right_of_neg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `log_neg` `log_lt_log_iff`
`logb_lt_logb_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`logb`	—	`logb.eq_1` `div_lt_div_right_of_neg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `log_neg` `log_lt_log`
`logb_mul` 📖	mathematical	—	`logb` `Real` `instMul` `instAdd`	—	`log_mul` `add_div`
`logb_mul_base` 📖	mathematical	—	`logb` `Real` `instMul` `instInv` `instAdd`	—	`inv_logb_mul_base` `inv_inv`
`logb_nat_eq_sum_factorization` 📖	mathematical	—	`logb` `Real` `instNatCast` `Finsupp.sum` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instAddCommMonoid` `Nat.factorization` `instMul`	—	`log_nat_eq_sum_factorization` `Finset.sum_congr` `Finset.sum_div` `mul_div_assoc'`
`logb_ne_zero_of_pos_of_ne_one` 📖	—	`Real` `instLT` `instOne` `instZero`	—	—	`eq_one_of_pos_of_logb_eq_zero`
`logb_ne_zero_of_pos_of_ne_one_of_base_lt_one` 📖	—	`Real` `instLT` `instZero` `instOne`	—	—	`eq_one_of_pos_of_logb_eq_zero_of_base_lt_one`
`logb_neg` 📖	mathematical	`Real` `instLT` `instOne` `instZero`	`logb`	—	`logb_neg_iff`
`logb_neg_base_eq_logb` 📖	mathematical	—	`logb` `Real` `instNeg`	—	`logb_abs_base` `abs_neg`
`logb_neg_eq_logb` 📖	mathematical	—	`logb` `Real` `instNeg`	—	`logb_abs` `abs_neg`
`logb_neg_iff` 📖	mathematical	`Real` `instLT` `instOne` `instZero`	`logb`	—	`logb_one` `logb_lt_logb_iff` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`logb_neg_iff_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`logb`	—	`logb_one` `logb_lt_logb_iff_of_base_lt_one` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`logb_neg_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`logb`	—	`logb_neg_iff_of_base_lt_one` `lt_trans` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`logb_nonneg` 📖	mathematical	`Real` `instLT` `instOne` `instLE`	`instZero` `logb`	—	`logb_nonneg_iff` `LT.lt.trans_le` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`logb_nonneg_iff` 📖	mathematical	`Real` `instLT` `instOne` `instZero`	`instLE` `logb`	—	`not_lt` `logb_neg_iff`
`logb_nonneg_iff_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`instLE` `logb`	—	`not_lt` `logb_neg_iff_of_base_lt_one`
`logb_nonneg_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne` `instLE`	`logb`	—	`logb_nonneg_iff_of_base_lt_one`
`logb_nonpos` 📖	mathematical	`Real` `instLT` `instOne` `instLE` `instZero`	`logb`	—	`logb_nonpos_iff'`
`logb_nonpos_iff` 📖	mathematical	`Real` `instLT` `instOne` `instZero`	`instLE` `logb`	—	`not_lt` `logb_pos_iff`
`logb_nonpos_iff'` 📖	mathematical	`Real` `instLT` `instOne` `instLE` `instZero`	`logb`	—	`LE.le.eq_or_lt` `logb_zero` `instZeroLEOneClass` `logb_nonpos_iff`
`logb_nonpos_iff_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`instLE` `logb`	—	`not_lt` `logb_pos_iff_of_base_lt_one`
`logb_one` 📖	mathematical	—	`logb` `Real` `instOne` `instZero`	—	`log_one` `zero_div`
`logb_one_left` 📖	mathematical	—	`logb` `Real` `instOne` `instZero`	—	`log_one` `div_zero`
`logb_one_left_eq_zero` 📖	mathematical	—	`logb` `Real` `instOne` `Pi.instZero` `instZero`	—	`logb_one_left` `Pi.zero_apply`
`logb_pos` 📖	mathematical	`Real` `instLT` `instOne`	`instZero` `logb`	—	`logb_pos_iff` `lt_trans` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`logb_pos_iff` 📖	mathematical	`Real` `instLT` `instOne` `instZero`	`logb`	—	`logb_one` `logb_lt_logb_iff` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`logb_pos_iff_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`logb`	—	`logb_one` `logb_lt_logb_iff_of_base_lt_one` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`logb_pos_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`logb`	—	`logb_pos_iff_of_base_lt_one`
`logb_pow` 📖	mathematical	—	`logb` `Real` `Monoid.toNatPow` `instMonoid` `instMul` `instNatCast`	—	`logb.eq_1` `log_pow` `mul_div_assoc`
`logb_prod` 📖	mathematical	—	`logb` `Finset.prod` `Real` `instCommMonoid` `Finset.sum` `instAddCommMonoid`	—	`Finset.cons_induction_on` `logb_one` `Finset.prod_cons` `logb_mul` `instNontrivial` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Finset.sum_cons`
`logb_rpow` 📖	mathematical	`Real` `instLT` `instZero`	`logb` `instPow`	—	`logb.eq_1` `div_eq_iff` `log_ne_zero_of_pos_of_ne_one` `log_rpow`
`logb_rpow_eq_mul_logb_of_pos` 📖	mathematical	`Real` `instLT` `instZero`	`logb` `instPow` `instMul`	—	`logb.eq_1` `log_rpow` `mul_div_assoc`
`logb_self_eq_one` 📖	mathematical	`Real` `instLT` `instOne`	`logb`	—	`div_self` `LT.lt.ne'` `log_pos`
`logb_self_eq_one_iff` 📖	mathematical	—	`logb` `Real` `instOne`	—	`div_zero` `NeZero.charZero_one` `RCLike.charZero_rclike` `div_self` `log_ne_zero`
`logb_surjective` 📖	mathematical	`Real` `instLT` `instZero`	`logb`	—	`logb_rpow`
`logb_zero` 📖	mathematical	—	`logb` `Real` `instZero`	—	`log_zero` `zero_div`
`logb_zero_left` 📖	mathematical	—	`logb` `Real` `instZero`	—	`log_zero` `div_zero`
`logb_zero_left_eq_zero` 📖	mathematical	—	`logb` `Real` `instZero` `Pi.instZero`	—	`logb_zero_left` `Pi.zero_apply`
`lt_logb_iff_rpow_lt` 📖	mathematical	`Real` `instLT` `instOne` `instZero`	`logb` `instPow`	—	`rpow_lt_rpow_left_iff` `rpow_logb`
`lt_logb_iff_rpow_lt_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`logb` `instPow`	—	`rpow_lt_rpow_left_iff_of_base_lt_one` `rpow_logb`
`mul_logb` 📖	mathematical	—	`Real` `instMul` `logb`	—	`mul_comm` `div_mul_div_cancel₀` `log_ne_zero`
`natCeil_logb_natCast` 📖	mathematical	—	`Nat.ceil` `Real` `semiring` `partialOrder` `FloorRing.toFloorSemiring` `instRing` `linearOrder` `instIsStrictOrderedRing` `instFloorRing` `logb` `instNatCast` `Nat.clog`	—	`instIsStrictOrderedRing` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `log_zero` `div_zero` `Nat.ceil_zero` `Nat.clog_zero_left` `zero_add` `Nat.cast_one` `log_one` `Nat.clog_one_left` `eq_or_ne` `Nat.cast_add` `logb_zero` `Nat.clog_zero_right` `Int.instCharZero` `Int.natCast_ceil_eq_ceil` `logb_nonneg` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `instZeroLEOneClass` `NeZero.charZero_one` `Nat.one_le_cast` `ceil_logb_natCast` `instIsOrderedRing` `Int.clog_natCast`
`natFloor_logb_natCast` 📖	mathematical	—	`Nat.floor` `Real` `semiring` `partialOrder` `FloorRing.toFloorSemiring` `instRing` `linearOrder` `instIsStrictOrderedRing` `instFloorRing` `logb` `instNatCast` `Nat.log`	—	`instIsStrictOrderedRing` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `log_zero` `div_zero` `Nat.floor_zero` `Nat.log_zero_left` `zero_add` `Nat.cast_one` `log_one` `Nat.log_one_left` `eq_or_ne` `Nat.cast_add` `logb_zero` `Nat.log_zero_right` `Int.instCharZero` `Int.natCast_floor_eq_floor` `logb_nonneg` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `instZeroLEOneClass` `NeZero.charZero_one` `Nat.one_le_cast` `floor_logb_natCast` `instIsOrderedRing` `Int.log_natCast`
`natLog_le_logb` 📖	mathematical	—	`Real` `instLE` `instNatCast` `Nat.log` `logb`	—	`le_trans` `instIsStrictOrderedRing` `floor_logb_natCast` `Nat.cast_nonneg` `instIsOrderedRing` `Int.log_natCast` `Int.cast_natCast` `le_refl` `Int.floor_le`
`range_logb` 📖	mathematical	`Real` `instLT` `instZero`	`Set.range` `logb` `Set.univ`	—	`Function.Surjective.range_eq` `logb_surjective`
`rpow_logb` 📖	mathematical	`Real` `instLT` `instZero`	`instPow` `logb`	—	`rpow_logb_eq_abs` `LT.lt.ne'` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`rpow_logb_eq_abs` 📖	mathematical	`Real` `instLT` `instZero`	`instPow` `logb` `abs` `lattice` `instAddGroup`	—	`log_injOn_pos` `rpow_pos_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `log_rpow` `logb.eq_1` `log_abs` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `log_ne_zero_of_pos_of_ne_one` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf`
`rpow_logb_of_neg` 📖	mathematical	`Real` `instLT` `instZero`	`instPow` `logb` `instNeg`	—	`rpow_logb_eq_abs` `ne_of_lt` `abs_of_neg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`strictAntiOn_logb` 📖	mathematical	`Real` `instLT` `instOne`	`StrictAntiOn` `instPreorder` `logb` `Set.Iio` `instZero`	—	`logb_abs` `logb_lt_logb` `abs_pos` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `LT.lt.ne` `abs_of_neg` `neg_lt_neg_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`strictAntiOn_logb_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`StrictAntiOn` `instPreorder` `logb` `Set.Ioi`	—	`logb_lt_logb_of_base_lt_one`
`strictMonoOn_logb` 📖	mathematical	`Real` `instLT` `instOne`	`StrictMonoOn` `instPreorder` `logb` `Set.Ioi` `instZero`	—	`logb_lt_logb`
`strictMonoOn_logb_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`StrictMonoOn` `instPreorder` `logb` `Set.Iio`	—	`logb_abs` `logb_lt_logb_of_base_lt_one` `abs_pos` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `LT.lt.ne` `abs_of_neg` `neg_lt_neg_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`surjOn_logb` 📖	mathematical	`Real` `instLT` `instZero`	`Set.SurjOn` `logb` `Set.Ioi` `instPreorder` `Set.univ`	—	`rpow_pos_of_pos` `logb_rpow`
`surjOn_logb'` 📖	mathematical	`Real` `instLT` `instZero`	`Set.SurjOn` `logb` `Set.Iio` `instPreorder` `Set.univ`	—	`IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `rpow_pos_of_pos` `logb_neg_eq_logb` `logb_rpow`
`tendsto_abs_logb_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `abs` `lattice` `instAddGroup` `logb` `Filter.atTop` `instPreorder`	—	`Filter.Tendsto.congr'` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `logb_nonneg` `tendsto_logb_atTop` `Filter.Tendsto.congr` `logb_inv_base` `abs_neg` `inv_neg` `inv_one` `inv_zero` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `one_lt_inv₀` `lt_of_not_ge` `lt_or_gt_of_ne` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_neg` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `instIsOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `le_of_not_gt` `logb_neg_base_eq_logb` `neg_neg` `neg_zero`
`tendsto_logb_atTop` 📖	mathematical	`Real` `instLT` `instOne`	`Filter.Tendsto` `logb` `Filter.atTop` `instPreorder`	—	`Filter.Tendsto.atTop_div_const` `instIsStrictOrderedRing` `log_pos` `tendsto_log_atTop`
`tendsto_logb_atTop_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`Filter.Tendsto` `logb` `Filter.atTop` `instPreorder` `Filter.atBot`	—	`Filter.tendsto_atTop_atBot` `instIsDirectedOrder` `instIsOrderedRing` `instArchimedean` `logb_le_iff_le_rpow_of_base_lt_one` `lt_of_lt_of_le` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`tendsto_logb_comp_add_sub_logb` 📖	mathematical	—	`Filter.Tendsto` `Real` `instSub` `logb` `instAdd` `Filter.atTop` `instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero`	—	`sub_div` `zero_div` `Filter.Tendsto.div_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_log_comp_add_sub_log`
`tendsto_logb_nat_add_one_sub_logb` 📖	mathematical	—	`Filter.Tendsto` `Real` `instSub` `logb` `instAdd` `instNatCast` `instOne` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero`	—	`Filter.Tendsto.comp` `tendsto_logb_comp_add_sub_logb` `tendsto_natCast_atTop_atTop` `instIsOrderedRing` `instArchimedean`
`tendsto_logb_nhdsGT_zero` 📖	mathematical	`Real` `instLT` `instOne`	`Filter.Tendsto` `logb` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero` `Set.Ioi` `instPreorder` `Filter.atBot`	—	`Filter.Tendsto.atBot_div_const` `instIsStrictOrderedRing` `log_pos` `tendsto_log_nhdsGT_zero`
`tendsto_logb_nhdsGT_zero_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`Filter.Tendsto` `logb` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `Set.Ioi` `instPreorder` `Filter.atTop`	—	`Filter.Tendsto.atBot_mul_const_of_neg` `instIsStrictOrderedRing` `inv_lt_zero` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `log_neg` `tendsto_log_nhdsGT_zero`
`tendsto_logb_nhdsNE_zero` 📖	mathematical	`Real` `instLT` `instOne`	`Filter.Tendsto` `logb` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.atBot` `instPreorder`	—	`Filter.Tendsto.atBot_div_const` `instIsStrictOrderedRing` `log_pos` `tendsto_log_nhdsNE_zero`
`tendsto_logb_nhdsNE_zero_of_base_lt_one` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`Filter.Tendsto` `logb` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.atTop` `instPreorder`	—	`Filter.Tendsto.atBot_mul_const_of_neg` `instIsStrictOrderedRing` `inv_lt_zero` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `log_neg` `tendsto_log_nhdsNE_zero`
`tendsto_pow_logb_div_mul_add_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `instMonoid` `logb` `instAdd` `instMul` `Filter.atTop` `instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero`	—	`eq_or_ne` `div_zero` `MulZeroClass.mul_zero` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_mul_add_inv_atTop_nhds_zero` `Filter.Tendsto.congr` `div_pow` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `tendsto_pow_log_div_mul_add_atTop` `mul_ne_zero`

---

← Back to Index