Repository navigation

Generalize the sum to `(n : R) ^ k * x ^ n` from `(n : R) ^ 2 * x ^ n` - #1

Merged

pepamontero merged 2 commits into

pepamontero:SpecificLimits-LogosWSfrom

Mal-Pat:SpecificLimits-LogosWS

Jul 10, 2026

Merged

Generalize the sum to `(n : R) ^ k * x ^ n` from `(n : R) ^ 2 * x ^ n`#1
pepamontero merged 2 commits into
pepamontero:SpecificLimits-LogosWSfrom
Mal-Pat:SpecificLimits-LogosWS

Commits on Jul 10, 2026
- Add theorem `pow_eq_sum_stirlingSecond_mul_descFactorial` in `Stirling.lean`
  Mal-Pat
  committed
  87aeaf7
- Generalize the sum to `(n : R) ^ k * x ^ n` from `(n : R) ^ 2 * x ^ n`
  Mal-Pat
  committed
  517f05b