∀ (𝕂 : Type u_1) (𝔸 : Type u_2) [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸],
  NormedSpace.expSeries 𝕂 𝔸 = FormalMultilinearSeries.ofScalars 𝔸 fun n => (↑n.factorial)⁻¹