Theorem Nat.descFactorial_mul_self

Modification history

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