∀ (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [inst : RCLike 𝕂] [inst_1 : NormedCommRing 𝕊] [inst_2 : NormedRing 𝔸]
  [inst_3 : NormedAlgebra 𝕂 𝕊] [inst_4 : NormedAlgebra 𝕂 𝔸] [inst_5 : Algebra 𝕊 𝔸] [inst_6 : ContinuousSMul 𝕊 𝔸]
  [inst_7 : IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊),
  HasStrictFDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) • ContinuousLinearMap.smulRight 1 x) t