Commit 2026-01-22 16:40 94d40e83
View on Github →feat(RingTheory/PowerSeries): split off Exp.lean (#34256)
The new file RingTheory/PowerSeries/Exp.lean takes definition and theorems from
RingTheory/PowerSeries/Wellknown.lean, and tweaks one
import in NumberTheory/Bernoulli.lean.