PolynomialExp

Statistics

Metric	Count
Definitions	0
Theorems `tendsto_div_exp_atTop`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_div_exp_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `eval` `Real.semiring` `Real.exp` `Filter.atTop` `Real.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`induction_on'` `eval_add` `add_div` `add_zero` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `eval_monomial` `div_eq_mul_inv` `mul_assoc` `Real.exp_neg` `MulZeroClass.mul_zero` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `tendsto_const_nhds` `Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero`

---