∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R]
  {f : MvPowerSeries σ R}, IsTopologicallyNilpotent (MvPowerSeries.constantCoeff f) → IsTopologicallyNilpotent f