mathlib3

278a14b3 - feat(analysis/p_series): prove the p-series convergence test (#4360)