mathlib3

283aafff - feat(ring_theory/power_series/well_known): power of exponential (#6330)

feat(ring_theory/power_series/well_known): power of exponential (#6330) Co-authored by Fabian Kruse Co-authored-by: Moritz Firsching <moritz.firsching@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>