mathlib3

f78693db - chore(data/complex/exponential): linting and pp_nodot (#3045)