Typo in documentation of `log_stirling_seq_formula`

Stream: general

[Naruyoko]

I was just browsing through mathlib and case across log_stirling_seq_formula:

We have the expression
log (stirling_seq (n + 1)) = log(n + 1)! - 1 / 2 * log(2 * n) - n * log ((n + 1) / e).

The formula is wrong, it should be log (stirling_seq (n + 1)) = log(n + 1)! - 1 / 2 * log(2 * (n + 1)) - (n + 1) * log ((n + 1) / e). It seems to be from copying it and forgetting to change n with n + 1 in some places.

[Patrick Massot]

See #6280.

[Eric Wieser]

Is there a reason to not just replace n + 1 with n? It's still true there (I pushed a commit, feel free to revert)

[Eric Wieser]

@Naruyoko, it sounds like you're reading the mathlib3 docs. Those will not be fixed, you should move to mathlib4

[Patrick Massot]

Eric, I did only a syntactic read and edit, without thinking about the math. I guess the only goal of that file it to get something from Freek's list, so that would be the very last declaration. I checked it isn't imported anywhere.

[Eric Wieser]

without thinking about the math

In your defence I think the 0 case is not math but Lean junk value coincidence