mathlib

1cd2bf58 - feat(analysis/special_functions/log/deriv): more power series for log (#14881)

feat(analysis/special_functions/log/deriv): more power series for log (#14881) This adds a power series expansion for `log ((a + 1) / a)`, and two lemmas that are needed for it. It's planned to be used in the proof of the Stirling formula. Co-authored-by: nick-kuhn <46423253+nick-kuhn@users.noreply.github.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: nick-kuhn <46423253+nick-kuhn@users.noreply.github.com>