Exponential

📁 Source: Mathlib/Combinatorics/Derangements/Exponential.lean

Statistics

Metric	Count
Definitions	0
Theorems numDerangements_tendsto_inv_e	1
Total	1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
numDerangements_tendsto_inv_e 📖	mathematical	—	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast numDerangements Nat.factorial Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.exp Real.instNeg Real.instOne	—	Int.cast_natCast numDerangements_sum Int.cast_sum Finset.sum_congr Int.cast_mul Int.cast_pow Int.cast_neg Int.cast_one Finset.sum_div refl IsPreorder.toRefl IsEquiv.toIsPreorder eq_isEquiv Finset.mem_range_succ_iff Nat.ascFactorial_eq_div add_tsub_cancel_of_le StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub Nat.cast_div_charZero RCLike.charZero_rclike Nat.factorial_dvd_factorial 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.mul_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.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Nat.cast_pos' Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one Nat.factorial_pos Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_ne_zero pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Mathlib.Meta.Positivity.nz_of_isNegNat Real.instIsStrictOrderedRing Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Filter.tendsto_add_atTop_iff_nat HasSum.tendsto_sum_nat instIsTopologicalRingReal Real.exp_eq_exp_ℝ NormedSpace.expSeries_div_hasSum_exp Real.instCompleteSpace

---

← Back to Index