mathlib

f5f7a3cf - feat(analysis/special_functions/exp_log): power series for log around 1 (#2646)

feat(analysis/special_functions/exp_log): power series for log around 1 (#2646) This PR adds the power series expansion for the real logarithm around `1`, in the form ```lean has_sum (λ (n : ℕ), x ^ (n + 1) / (n + 1)) (-log (1 - x)) ```