Theorem Nat.pow_eq_sum_stirlingSecond_mul_descFactorial

Modification history

2026-08-13 13:53
Mathlib/Combinatorics/Enumerative/Stirling.lean
feat(Analysis/SpecificLimits/Normed): the sum ∑' n, n ^ k * r ^ n via Stirling numbers (#41498) …
Added Nat.pow_eq_sum_stirlingSecond_mul_descFactorialView on Github →