Documentation Verification Report

ExponentialBounds

📁 Source: Mathlib/Analysis/Complex/ExponentialBounds.lean

Statistics

Metric	Count
Definitions	0
Theorems `ceil_exp_one_eq_three`, `exp_neg_one_gt_d9`, `exp_neg_one_lt_d9`, `exp_neg_one_lt_half`, `exp_one_gt_d9`, `exp_one_gt_two`, `exp_one_lt_d9`, `exp_one_lt_three`, `exp_one_near_10`, `exp_one_near_20`, `floor_exp_one_eq_two`, `log_two_gt_d9`, `log_two_lt_d9`, `log_two_near_10`, `round_exp_one_eq_three`	15
Total	15

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ceil_exp_one_eq_three` 📖	mathematical	—	`Int.ceil` `Real` `instRing` `linearOrder` `instFloorRing` `exp` `instOne`	—	`Int.ceil_eq_iff` `Nat.instAtLeastTwoHAddOfNat` `Nat.cast_one` `Int.cast_one` `exp_one_gt_two` `LT.lt.le` `exp_one_lt_three`
`exp_neg_one_gt_d9` 📖	mathematical	—	`Real` `instLT` `NNRatCast.toOfScientific` `instNNRatCast` `exp` `instNeg` `instOne`	—	`exp_neg` `lt_inv_comm₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `exp_pos` `lt_of_le_of_lt` `Nat.instAtLeastTwoHAddOfNat` `sub_le_iff_le_add` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `abs_sub_le_iff` `exp_one_near_10` `Mathlib.Meta.NormNum.isNNRat_add` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo`
`exp_neg_one_lt_d9` 📖	mathematical	—	`Real` `instLT` `exp` `instNeg` `instOne` `NNRatCast.toOfScientific` `instNNRatCast`	—	`exp_neg` `inv_lt_comm₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `exp_pos` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `lt_of_lt_of_le` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_one` `sub_le_comm` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `abs_sub_le_iff` `exp_one_near_10`
`exp_neg_one_lt_half` 📖	mathematical	—	`Real` `instLT` `exp` `instNeg` `instOne` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`lt_trans` `Nat.instAtLeastTwoHAddOfNat` `exp_neg_one_lt_d9` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo`
`exp_one_gt_d9` 📖	mathematical	—	`Real` `instLT` `NNRatCast.toOfScientific` `instNNRatCast` `exp` `instOne`	—	`lt_of_lt_of_le` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_one` `sub_le_comm` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `abs_sub_le_iff` `exp_one_near_10`
`exp_one_gt_two` 📖	mathematical	—	`Real` `instLT` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `exp` `instOne`	—	`lt_trans` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `exp_one_gt_d9`
`exp_one_lt_d9` 📖	mathematical	—	`Real` `instLT` `exp` `instOne` `NNRatCast.toOfScientific` `instNNRatCast`	—	`lt_of_le_of_lt` `Nat.instAtLeastTwoHAddOfNat` `sub_le_iff_le_add` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `abs_sub_le_iff` `exp_one_near_10` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Rat.instCharZero`
`exp_one_lt_three` 📖	mathematical	—	`Real` `instLT` `exp` `instOne` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`lt_trans` `Nat.instAtLeastTwoHAddOfNat` `exp_one_lt_d9` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `Mathlib.Meta.NormNum.instAtLeastTwo`
`exp_one_near_10` 📖	mathematical	—	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `exp` `instOne` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `instMonoid`	—	`exp_approx_start` `Nat.instAtLeastTwoHAddOfNat` `exp_1_approx_succ_eq` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `exp_approx_end'` `abs_one` `instIsOrderedRing` `Mathlib.Meta.NormNum.isRat_le_true` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_abs_nonneg` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.isNat_abs_nonneg`
`exp_one_near_20` 📖	mathematical	—	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `exp` `instOne` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `instMonoid`	—	`exp_approx_start` `Nat.instAtLeastTwoHAddOfNat` `exp_1_approx_succ_eq` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `exp_approx_end'` `abs_one` `instIsOrderedRing` `Mathlib.Meta.NormNum.isRat_le_true` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_abs_nonneg` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.isNat_abs_nonneg`
`floor_exp_one_eq_two` 📖	mathematical	—	`Int.floor` `Real` `instRing` `linearOrder` `instFloorRing` `exp` `instOne`	—	`Int.floor_eq_iff` `LT.lt.le` `Nat.instAtLeastTwoHAddOfNat` `exp_one_gt_two` `Nat.cast_one` `Int.cast_one` `Int.cast_natCast` `exp_one_lt_three`
`log_two_gt_d9` 📖	mathematical	—	`Real` `instLT` `NNRatCast.toOfScientific` `instNNRatCast` `log` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`lt_of_lt_of_le` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_one` `sub_le_comm` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `abs_sub_le_iff` `log_two_near_10`
`log_two_lt_d9` 📖	mathematical	—	`Real` `instLT` `log` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `NNRatCast.toOfScientific` `instNNRatCast`	—	`lt_of_le_of_lt` `Nat.instAtLeastTwoHAddOfNat` `sub_le_iff_le_add` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `abs_sub_le_iff` `log_two_near_10` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `Rat.instCharZero`
`log_two_near_10` 📖	mathematical	—	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `log` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `Monoid.toNatPow` `instMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.instAtLeastTwo` `abs_log_sub_add_sum_range_le` `Nat.cast_one` `le_trans` `abs_sub_le` `add_le_add` `covariant_swap_add_of_covariant_add` `abs_sub_comm` `sub_eq_add_neg` `log_inv` `one_div` `Finset.sum_congr` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.one_natPow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Finset.sum_range_succ` `Mathlib.Meta.NormNum.natPow_one` `Mathlib.Meta.NormNum.isNat_natCast` `zero_add` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_abs_nonneg` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.isRat_le_true`
`round_exp_one_eq_three` 📖	mathematical	—	`round` `Real` `instRing` `linearOrder` `instFloorRing` `exp` `instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `round_eq` `instIsStrictOrderedRing` `Int.floor_eq_iff` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `le_of_lt` `exp_one_gt_d9` `Mathlib.Meta.NormNum.isRat_le_true` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_intCast` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNat_intOfNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo`

---

← Back to Index