∀ (𝕜 : Type u) {𝕜' : Type u'} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : Semiring 𝕜'] [inst_12 : SMul 𝕜 𝕜'] [inst_13 : Module 𝕜' E]
  [inst_14 : ContinuousConstSMul 𝕜' E] [inst_15 : IsScalarTower 𝕜 𝕜' E] [inst_16 : Module 𝕜' F]
  [inst_17 : ContinuousConstSMul 𝕜' F] [inst_18 : IsScalarTower 𝕜 𝕜' F] (p : FormalMultilinearSeries 𝕜' E F) (n : ℕ),
  FormalMultilinearSeries.restrictScalars 𝕜 p n = ContinuousMultilinearMap.restrictScalars 𝕜 (p n)