Exp

📁 Source: Mathlib/Analysis/SpecialFunctions/Exp.lean

Statistics

Metric	Count
Definitions `expOrderIso`	1
Theorems `comap_exp_cobounded`, `comap_exp_nhdsNE`, `comap_exp_nhds_zero`, `continuousOn_exp`, `continuous_exp`, `exp_bound_sq`, `exp_sub_sum_range_isBigO_pow`, `exp_sub_sum_range_succ_isLittleO_pow`, `locally_lipschitz_exp`, `tendsto_exp_comap_re_atBot`, `tendsto_exp_comap_re_atBot_nhdsNE`, `tendsto_exp_comap_re_atTop`, `tendsto_exp_nhds_zero_iff`, `cexp`, `rexp`, `cexp`, `rexp`, `cexp`, `rexp`, `cexp`, `rexp`, `cexp`, `rexp`, `cexp`, `rexp`, `coe_comp_expOrderIso`, `coe_expOrderIso_apply`, `comap_exp_atTop`, `comap_exp_nhdsGT_zero`, `comap_exp_nhds_exp`, `comap_exp_nhds_zero`, `continuousOn_exp`, `continuous_exp`, `exp_half`, `exp_sub_sum_range_isBigO_pow`, `exp_sub_sum_range_succ_isLittleO_pow`, `isBigO_exp_comp_exp_comp`, `isBigO_exp_comp_one`, `isBigO_one_exp_comp`, `isBoundedUnder_ge_exp_comp`, `isBoundedUnder_le_exp_comp`, `isLittleO_exp_comp_exp_comp`, `isLittleO_one_exp_comp`, `isLittleO_pow_exp_atTop`, `isOpenEmbedding_exp`, `isTheta_exp_comp_exp_comp`, `isTheta_exp_comp_one`, `map_exp_atBot`, `map_exp_atTop`, `map_exp_nhds`, `mul_exp_neg_le_exp_neg_one`, `range_exp`, `summable_exp_nat_mul_iff`, `summable_exp_nat_mul_of_ge`, `summable_exp_neg_nat`, `summable_pow_mul_exp_neg_nat_mul`, `tendsto_comp_exp_atBot`, `tendsto_comp_exp_atTop`, `tendsto_div_pow_mul_exp_add_atTop`, `tendsto_exp_atBot`, `tendsto_exp_atBot_nhdsGT`, `tendsto_exp_atTop`, `tendsto_exp_comp_atTop`, `tendsto_exp_comp_nhds_zero`, `tendsto_exp_div_pow_atTop`, `tendsto_exp_neg_atTop_nhds_zero`, `tendsto_exp_nhds_zero_nhds_one`, `tendsto_mul_exp_add_div_pow_atTop`, `tendsto_pow_mul_exp_neg_atTop_nhds_zero`, `cexp`	70
Total	71

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_exp_cobounded` 📖	mathematical	—	`Filter.comap` `Complex` `exp` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `Real` `re` `Filter.atTop` `Real.instPreorder`	—	`Filter.comap_comap` `norm_exp` `Real.comap_exp_atTop`
`comap_exp_nhdsNE` 📖	mathematical	—	`Filter.comap` `Complex` `exp` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instZero` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Real` `re` `Filter.atBot` `Real.instPreorder`	—	`Set.eq_univ_of_forall` `exp_ne_zero` `Filter.comap_inf` `comap_exp_nhds_zero` `Filter.comap_principal` `Filter.principal_univ` `inf_of_le_left`
`comap_exp_nhds_zero` 📖	mathematical	—	`Filter.comap` `Complex` `exp` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instZero` `Real` `re` `Filter.atBot` `Real.instPreorder`	—	`comap_norm_nhds_zero` `Filter.comap_comap` `norm_exp` `Real.comap_exp_nhds_zero`
`continuousOn_exp` 📖	mathematical	—	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `exp`	—	`Continuous.continuousOn` `continuous_exp`
`continuous_exp` 📖	mathematical	—	`Continuous` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `exp`	—	`continuous_iff_continuousAt` `continuousAt_of_locally_lipschitz` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Nat.instAtLeastTwoHAddOfNat` `dist_eq_norm` `one_add_one_eq_two` `locally_lipschitz_exp` `zero_le_one` `le_rfl`
`exp_bound_sq` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `Complex` `instNorm` `Real.instOne`	`instSub` `exp` `instAdd` `Algebra.toSMul` `instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	—	`exp_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `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_add_gt` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `norm_mul` `NormedDivisionRing.toNormMulClass` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_exp_sub_one_sub_id_le` `norm_nonneg`
`exp_sub_sum_range_isBigO_pow` 📖	mathematical	—	`Asymptotics.IsBigO` `Complex` `instNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instZero` `instSub` `exp` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `Finset.range` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNatCast` `Nat.factorial`	—	`LE.le.eq_or_lt` `zero_le` `Nat.instCanonicallyOrderedAdd` `sub_zero` `pow_zero` `NormedDivisionRing.to_normOneClass` `Filter.Tendsto.isBoundedUnder_le` `BoundedLENhdsClass.of_closedIciTopology` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `ContinuousAt.norm` `Continuous.continuousAt` `continuous_exp` `Asymptotics.IsBigO.of_bound` `Filter.HasBasis.eventually_iff` `NormedAddCommGroup.nhds_zero_basis_norm_lt` `one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Nat.cast_add` `Nat.cast_one` `norm_pow` `NormedDivisionRing.toNormMulClass` `mul_inv_rev` `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.subst_add` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `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.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Nat.factorial_pos` `add_pos'` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `exp_bound` `LT.lt.le` `Membership.mem.out`
`exp_sub_sum_range_succ_isLittleO_pow` 📖	mathematical	—	`Asymptotics.IsLittleO` `Complex` `instNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instZero` `instSub` `exp` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `Finset.range` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNatCast` `Nat.factorial`	—	`Asymptotics.IsBigO.trans_isLittleO` `exp_sub_sum_range_isBigO_pow` `Asymptotics.isLittleO_pow_pow`
`locally_lipschitz_exp` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instOne` `Real.instLT` `Norm.norm` `Complex` `instNorm` `instSub`	`exp` `Real.instMul` `Real.instAdd`	—	`Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg` `pow_two` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `LT.lt.le` `le_rfl` `norm_nonneg` `exp_bound_sq` `sub_le_iff_le_add'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `norm_smul` `NormedSpace.toNormSMulClass` `LE.le.trans` `norm_sub_norm_le` `le_imp_le_of_le_of_le` `add_le_add_right` `mul_le_mul_of_nonneg_left` `le_refl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one`
`tendsto_exp_comap_re_atBot` 📖	mathematical	—	`Filter.Tendsto` `Complex` `exp` `Filter.comap` `Real` `re` `Filter.atBot` `Real.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instZero`	—	`Filter.tendsto_comap` `comap_exp_nhds_zero`
`tendsto_exp_comap_re_atBot_nhdsNE` 📖	mathematical	—	`Filter.Tendsto` `Complex` `exp` `Filter.comap` `Real` `re` `Filter.atBot` `Real.instPreorder` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instZero` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`Filter.tendsto_comap` `comap_exp_nhdsNE`
`tendsto_exp_comap_re_atTop` 📖	mathematical	—	`Filter.Tendsto` `Complex` `exp` `Filter.comap` `Real` `re` `Filter.atTop` `Real.instPreorder` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField`	—	`Filter.tendsto_comap` `comap_exp_cobounded`
`tendsto_exp_nhds_zero_iff` 📖	mathematical	—	`Filter.Tendsto` `Complex` `exp` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instZero` `Real` `re` `Filter.atBot` `Real.instPreorder`	—	`comap_exp_nhds_zero`

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cexp` 📖	mathematical	`Continuous` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`Complex.exp`	—	`continuous_iff_continuousAt` `ContinuousAt.cexp` `continuousAt`
`rexp` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.exp`	—	`continuous_iff_continuousAt` `ContinuousAt.rexp` `continuousAt`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cexp` 📖	mathematical	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`Complex.exp`	—	`Filter.Tendsto.cexp`
`rexp` 📖	mathematical	`ContinuousAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.exp`	—	`Filter.Tendsto.rexp`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cexp` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`Complex.exp`	—	`ContinuousWithinAt.cexp`
`rexp` 📖	mathematical	`ContinuousOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.exp`	—	`ContinuousWithinAt.rexp`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cexp` 📖	mathematical	`ContinuousWithinAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`Complex.exp`	—	`Filter.Tendsto.cexp`
`rexp` 📖	mathematical	`ContinuousWithinAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.exp`	—	`Filter.Tendsto.rexp`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cexp` 📖	mathematical	`Filter.Tendsto` `Complex` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`Complex.exp`	—	`comp` `Continuous.tendsto` `Complex.continuous_exp`
`rexp` 📖	mathematical	`Filter.Tendsto` `Real` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.exp`	—	`comp` `Continuous.tendsto` `Real.continuous_exp`

HasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cexp` 📖	mathematical	`HasSum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `SummationFilter.unconditional`	`HasProd` `CommRing.toCommMonoid` `Complex.commRing` `Complex.exp`	—	`Filter.Tendsto.congr` `Complex.exp_sum` `Filter.Tendsto.cexp`
`rexp` 📖	mathematical	`HasSum` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SummationFilter.unconditional`	`HasProd` `Real.instCommMonoid` `Real.exp`	—	`Filter.Tendsto.congr` `Real.exp_sum` `Filter.Tendsto.rexp`

Real

Definitions

Name	Category	Theorems
`expOrderIso` 📖	CompOp	4 math math: `coe_expOrderIso_apply`, `log_of_pos`, `coe_comp_expOrderIso`, `log_of_ne_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_comp_expOrderIso` 📖	mathematical	—	`Real` `Set.Elem` `Set.Ioi` `instPreorder` `instZero` `Set` `Set.instMembership` `DFunLike.coe` `OrderIso` `instLE` `instFunLikeOrderIso` `expOrderIso` `exp`	—	—
`coe_expOrderIso_apply` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `Set.Ioi` `instPreorder` `instZero` `DFunLike.coe` `OrderIso` `Set.Elem` `instLE` `instFunLikeOrderIso` `expOrderIso` `exp`	—	—
`comap_exp_atTop` 📖	mathematical	—	`Filter.comap` `Real` `exp` `Filter.atTop` `instPreorder`	—	`map_exp_atTop` `Filter.comap_map` `exp_injective`
`comap_exp_nhdsGT_zero` 📖	mathematical	—	`Filter.comap` `Real` `exp` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero` `Set.Ioi` `instPreorder` `Filter.atBot`	—	`map_exp_atBot` `Filter.comap_map` `exp_injective`
`comap_exp_nhds_exp` 📖	mathematical	—	`Filter.comap` `Real` `exp` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace`	—	`Topology.IsInducing.nhds_eq_comap` `Topology.IsEmbedding.toIsInducing` `Topology.IsOpenEmbedding.toIsEmbedding` `isOpenEmbedding_exp`
`comap_exp_nhds_zero` 📖	mathematical	—	`Filter.comap` `Real` `exp` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero` `Filter.atBot` `instPreorder`	—	`comap_nhdsWithin_range` `range_exp` `comap_exp_nhdsGT_zero`
`continuousOn_exp` 📖	mathematical	—	`ContinuousOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `exp`	—	`Continuous.continuousOn` `continuous_exp`
`continuous_exp` 📖	mathematical	—	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `exp`	—	`Continuous.comp'` `Complex.continuous_re` `Continuous.cexp` `Complex.continuous_ofReal`
`exp_half` 📖	mathematical	—	`exp` `Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `sqrt`	—	`Nat.instAtLeastTwoHAddOfNat` `sqrt_eq_iff_eq_sq` `LT.lt.le` `exp_pos` `sq` `exp_add` `add_halves` `CharZero.NeZero.two` `RCLike.charZero_rclike`
`exp_sub_sum_range_isBigO_pow` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero` `instSub` `exp` `Finset.sum` `instAddCommMonoid` `Finset.range` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `instMonoid` `instNatCast` `Nat.factorial`	—	`Asymptotics.IsBigO.comp_tendsto` `Complex.exp_sub_sum_range_isBigO_pow` `Continuous.tendsto'` `Complex.continuous_ofReal` `Nat.cast_zero` `Finset.sum_congr`
`exp_sub_sum_range_succ_isLittleO_pow` 📖	mathematical	—	`Asymptotics.IsLittleO` `Real` `norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero` `instSub` `exp` `Finset.sum` `instAddCommMonoid` `Finset.range` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `instMonoid` `instNatCast` `Nat.factorial`	—	`Asymptotics.IsBigO.trans_isLittleO` `exp_sub_sum_range_isBigO_pow` `Asymptotics.isLittleO_pow_pow`
`isBigO_exp_comp_exp_comp` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `norm` `exp` `Filter.IsBoundedUnder` `instLE` `Pi.instSub` `instSub`	—	`Asymptotics.isBigO_iff_isBoundedUnder_le_div` `Filter.Eventually.of_forall` `exp_ne_zero` `abs_exp`
`isBigO_exp_comp_one` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `norm` `exp` `instOne` `Filter.IsBoundedUnder` `instLE`	—	`NormedDivisionRing.to_normOneClass` `abs_exp`
`isBigO_one_exp_comp` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `norm` `instOne` `exp` `Filter.IsBoundedUnder` `instLE`	—	`zero_sub` `instIsOrderedAddMonoid`
`isBoundedUnder_ge_exp_comp` 📖	mathematical	—	`Filter.IsBoundedUnder` `Real` `instLE` `exp`	—	`Filter.isBoundedUnder_of` `LT.lt.le` `exp_pos`
`isBoundedUnder_le_exp_comp` 📖	mathematical	—	`Filter.IsBoundedUnder` `Real` `instLE` `exp`	—	`Monotone.isBoundedUnder_le_comp_iff` `instNoMaxOrderOfNontrivial` `instIsOrderedRing` `instNontrivial` `exp_monotone` `tendsto_exp_atTop`
`isLittleO_exp_comp_exp_comp` 📖	mathematical	—	`Asymptotics.IsLittleO` `Real` `norm` `exp` `Filter.Tendsto` `instSub` `Filter.atTop` `instPreorder`	—	`instIsOrderedAddMonoid` `neg_sub`
`isLittleO_one_exp_comp` 📖	mathematical	—	`Asymptotics.IsLittleO` `Real` `norm` `instOne` `exp` `Filter.Tendsto` `Filter.atTop` `instPreorder`	—	`sub_zero`
`isLittleO_pow_exp_atTop` 📖	mathematical	—	`Asymptotics.IsLittleO` `Real` `norm` `Filter.atTop` `instPreorder` `Monoid.toNatPow` `instMonoid` `exp`	—	`Asymptotics.isLittleO_iff_tendsto` `LT.lt.ne'` `exp_pos` `one_mul` `add_zero` `tendsto_div_pow_mul_exp_add_atTop` `zero_ne_one` `NeZero.charZero_one` `RCLike.charZero_rclike`
`isOpenEmbedding_exp` 📖	mathematical	—	`Topology.IsOpenEmbedding` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `exp`	—	`Topology.IsOpenEmbedding.comp` `instOrderTopologyReal` `orderTopology_of_ordConnected` `Set.ordConnected_Ioi` `IsOpen.isOpenEmbedding_subtypeVal` `isOpen_Ioi` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `Homeomorph.isOpenEmbedding`
`isTheta_exp_comp_exp_comp` 📖	mathematical	—	`Asymptotics.IsTheta` `Real` `norm` `exp` `Filter.IsBoundedUnder` `instLE` `abs` `lattice` `instAddGroup` `instSub`	—	`instIsOrderedAddMonoid` `neg_sub`
`isTheta_exp_comp_one` 📖	mathematical	—	`Asymptotics.IsTheta` `Real` `norm` `exp` `instOne` `Filter.IsBoundedUnder` `instLE` `abs` `lattice` `instAddGroup`	—	`sub_zero`
`map_exp_atBot` 📖	mathematical	—	`Filter.map` `Real` `exp` `Filter.atBot` `instPreorder` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero` `Set.Ioi`	—	`coe_comp_expOrderIso` `Filter.map_map` `OrderIso.map_atBot` `map_coe_Ioi_atBot` `instOrderTopologyReal` `Order.IsPredPrelimit.of_dense` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing`
`map_exp_atTop` 📖	mathematical	—	`Filter.map` `Real` `exp` `Filter.atTop` `instPreorder`	—	`coe_comp_expOrderIso` `Filter.map_map` `OrderIso.map_atTop` `Filter.map_val_Ioi_atTop` `instIsDirectedOrder` `instIsOrderedRing` `instArchimedean` `instNoMaxOrderOfNontrivial` `instNontrivial`
`map_exp_nhds` 📖	mathematical	—	`Filter.map` `Real` `exp` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace`	—	`Topology.IsOpenEmbedding.map_nhds_eq` `isOpenEmbedding_exp`
`mul_exp_neg_le_exp_neg_one` 📖	mathematical	—	`Real` `instLE` `instMul` `exp` `instNeg` `instOne`	—	`sub_add_cancel` `add_one_le_exp` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `instIsOrderedRing` `le_of_lt` `exp_pos` `sub_add_eq_add_sub` `add_neg_cancel` `zero_sub`
`range_exp` 📖	mathematical	—	`Set.range` `Real` `exp` `Set.Ioi` `instPreorder` `instZero`	—	`coe_comp_expOrderIso` `Set.range_comp` `OrderIso.range_eq` `Set.image_univ` `Subtype.range_coe`
`summable_exp_nat_mul_iff` 📖	mathematical	—	`Summable` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `exp` `instMul` `instNatCast` `SummationFilter.unconditional` `instLT` `instZero`	—	`exp_nat_mul` `norm_of_nonneg` `exp_nonneg`
`summable_exp_nat_mul_of_ge` 📖	mathematical	`Real` `instLT` `instZero` `instLE` `instNatCast`	`Summable` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `exp` `instMul` `SummationFilter.unconditional`	—	`Summable.of_nonneg_of_le` `le_of_lt` `exp_pos` `exp_monotone` `mul_comm` `mul_le_mul_of_nonpos_left` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `LT.lt.le` `summable_exp_nat_mul_iff`
`summable_exp_neg_nat` 📖	mathematical	—	`Summable` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `exp` `instNeg` `instNatCast` `SummationFilter.unconditional`	—	`mul_neg_one` `summable_exp_nat_mul_iff` `neg_one_lt_zero` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`summable_pow_mul_exp_neg_nat_mul` 📖	mathematical	`Real` `instLT` `instZero`	`Summable` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instMul` `Monoid.toNatPow` `instMonoid` `instNatCast` `exp` `instNeg` `SummationFilter.unconditional`	—	`mul_comm` `exp_nat_mul` `summable_pow_mul_geometric_of_norm_lt_one` `instHasSummableGeomSeries` `norm_of_nonneg` `exp_nonneg` `exp_lt_one_iff` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`tendsto_comp_exp_atBot` 📖	mathematical	—	`Filter.Tendsto` `Real` `exp` `Filter.atBot` `instPreorder` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero` `Set.Ioi`	—	`map_exp_atBot` `Filter.tendsto_map'_iff`
`tendsto_comp_exp_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `exp` `Filter.atTop` `instPreorder`	—	`map_exp_atTop`
`tendsto_div_pow_mul_exp_add_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `instMonoid` `instAdd` `instMul` `exp` `Filter.atTop` `instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero`	—	`inv_div` `Filter.Tendsto.inv_tendsto_atTop` `instIsStrictOrderedRing` `instOrderTopologyReal` `tendsto_mul_exp_add_div_pow_atTop` `lt_or_gt_of_ne` `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` `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.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `neg_mul` `mul_neg` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `neg_add` `div_neg` `neg_neg` `neg_zero` `Filter.Tendsto.neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`tendsto_exp_atBot` 📖	mathematical	—	`Filter.Tendsto` `Real` `exp` `Filter.atBot` `instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero`	—	`Filter.Tendsto.congr` `neg_neg` `Filter.Tendsto.comp` `tendsto_exp_neg_atTop_nhds_zero` `Filter.tendsto_neg_atBot_atTop` `instIsOrderedAddMonoid`
`tendsto_exp_atBot_nhdsGT` 📖	mathematical	—	`Filter.Tendsto` `Real` `exp` `Filter.atBot` `instPreorder` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero` `Set.Ioi`	—	`Filter.tendsto_inf` `tendsto_exp_atBot` `Filter.tendsto_principal` `Filter.Eventually.of_forall` `exp_pos`
`tendsto_exp_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `exp` `Filter.atTop` `instPreorder`	—	`Filter.tendsto_atTop_add_const_right` `instIsOrderedAddMonoid` `Filter.tendsto_id` `Filter.eventually_atTop` `instIsDirectedOrder` `instIsOrderedRing` `instArchimedean` `add_one_le_exp` `Filter.tendsto_atTop_mono'`
`tendsto_exp_comp_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `exp` `Filter.atTop` `instPreorder`	—	`comap_exp_atTop`
`tendsto_exp_comp_nhds_zero` 📖	mathematical	—	`Filter.Tendsto` `Real` `exp` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero` `Filter.atBot` `instPreorder`	—	`comap_exp_nhds_zero`
`tendsto_exp_div_pow_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `exp` `Monoid.toNatPow` `instMonoid` `Filter.atTop` `instPreorder`	—	`Filter.HasBasis.tendsto_iff` `Filter.atTop_basis_Ioi` `instIsDirectedOrder` `instIsOrderedRing` `instArchimedean` `instNoMaxOrderOfNontrivial` `instNontrivial` `Filter.atTop_basis'` `LT.lt.trans_le` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `mul_pos` `exp_pos` `Filter.eventually_atTop` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.eventually` `tendsto_pow_const_div_const_pow_of_one_lt` `one_lt_exp_iff` `gt_mem_nhds` `instOrderTopologyReal` `LE.le.trans_lt` `Nat.cast_nonneg` `Set.mem_Ioi` `Set.mem_Ici` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `pow_pos` `le_div_iff₀'` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `le_of_lt` `Nat.le_ceil` `Nat.cast_one` `LT.lt.le` `mul_one` `Nat.lt_ceil` `div_le_div_of_nonneg_right` `exp_monotone` `Nat.ceil_lt_add_one` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `add_comm` `exp_add` `mul_div_mul_left` `LT.lt.ne'`
`tendsto_exp_neg_atTop_nhds_zero` 📖	mathematical	—	`Filter.Tendsto` `Real` `exp` `instNeg` `Filter.atTop` `instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero`	—	`Filter.Tendsto.congr` `exp_neg` `Filter.Tendsto.comp` `tendsto_inv_atTop_zero` `instIsStrictOrderedRing` `instOrderTopologyReal` `tendsto_exp_atTop`
`tendsto_exp_nhds_zero_nhds_one` 📖	mathematical	—	`Filter.Tendsto` `Real` `exp` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero` `instOne`	—	`exp_zero` `Continuous.tendsto` `continuous_exp`
`tendsto_mul_exp_add_div_pow_atTop` 📖	mathematical	`Real` `instLT` `instZero`	`Filter.Tendsto` `DivInvMonoid.toDiv` `instDivInvMonoid` `instAdd` `instMul` `exp` `Monoid.toNatPow` `instMonoid` `Filter.atTop` `instPreorder`	—	`eq_or_ne` `pow_zero` `div_one` `Filter.Tendsto.atTop_add` `instIsOrderedAddMonoid` `instOrderTopologyReal` `Filter.Tendsto.const_mul_atTop` `instIsStrictOrderedRing` `tendsto_exp_atTop` `tendsto_const_nhds` `add_div` `mul_div_assoc` `tendsto_exp_div_pow_atTop` `Filter.Tendsto.div_atTop` `Filter.tendsto_pow_atTop` `instIsOrderedRing`
`tendsto_pow_mul_exp_neg_atTop_nhds_zero` 📖	mathematical	—	`Filter.Tendsto` `Real` `instMul` `Monoid.toNatPow` `instMonoid` `exp` `instNeg` `Filter.atTop` `instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instZero`	—	`Filter.Tendsto.congr` `inv_eq_one_div` `div_div_eq_mul_div` `one_mul` `div_eq_mul_inv` `exp_neg` `Filter.Tendsto.comp` `tendsto_inv_atTop_zero` `instIsStrictOrderedRing` `instOrderTopologyReal` `tendsto_exp_div_pow_atTop`

UniformContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cexp` 📖	mathematical	—	`UniformContinuousOn` `Complex` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.exp` `setOf` `Real` `Real.instLE` `Complex.re`	—	`Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Continuous.cexp` `continuous_id'` `continuous_one` `Metric.uniformContinuousOn_iff` `Nat.instAtLeastTwoHAddOfNat` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.exp_pos` `dist_sub_eq_dist_add_right` `sub_add_cancel` `Metric.continuous_iff'` `Metric.eventually_nhds_iff` `dist_zero_right` `dist_eq_norm` `mul_sub_one` `Complex.exp_add` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.add_congr` `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_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `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_zero_add` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `add_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `Mathlib.Tactic.RingNF.add_neg` `mul_comm` `Complex.norm_exp` `norm_mul` `NormedDivisionRing.toNormMulClass` `lt_of_le_of_lt` `mul_le_mul` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `LT.lt.le` `Complex.exp_zero` `Real.exp_nonneg` `Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt` `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.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `LT.lt.ne'` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.cons_pos` `Real.instZeroLEOneClass` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `RCLike.charZero_rclike`

---

← Back to Index