mathlib3

8b5ff9ce - feat(analysis/special_functions/integrals): `integral_log` (#7732)

feat(analysis/special_functions/integrals): `integral_log` (#7732) The integral of the (real) logarithmic function over the interval `[a, b]`, provided that `0 ∉ interval a b`.