формальная теорема о делении Вейерштрасса
Утверждение:

Пусть F -- формальный степенной ряд из K[[x1,x2,...xn,t]]
регулярный степени m по t, то есть F(0,...0,t)=a_m*t^m + a_{m+1}*t^{m+1} ...
Тогда любой ряд P можно единственным образом записать в виде P=Q*F+R
где R -- ряд, который как ряд K[[x1,x2,...xn]][[t]] является многочленом по t степени меньше m.


Доказательство:

Лемма 1. Пусть A -- полная неархимедово нормированная (на всякий случай абелева) группа c дискретным нормированием,
то есть норма принимает значения среди 1/2^n.
f -- непрерывный эндоморфизм A , такой что (Id-f) -- сжимающее отображение
(то есть в нашем дискретном случае это значит просто что Id-f уменьшает норму в 2 или больше раз).
Тогда f -- автоморфизм.

Док-во леммы 1.
Если x\in Ker f, то x меньше любого положительного числа и значит равно 0.
Для сюръекции: пусть x -- произвольный элемент из A. Рассмотрим последовательность
итераций (Id-f)^n(x), n>=0
(Id-f)^n(x) стремится к 0 по полноте, и так как норма неархимедова, то из этого
следует, что ряд Sum_n (Id-f)^n(x) сходится. По непрерывности
f(Sum_n (Id-f)^n(x))=Sum_n f(Id-f)^n(x)=Sum_n (Id-f)^n - (Id-f)^n+1 (x) = x

Определение. Пусть A -- полное нормированное кольцо, H -- аддитивная
подгруппа в нем. Элемент w\in A назовем элементом Вейерштрасса (в отношении H),
если A раскладывается в прямую сумму (как аддитивная группа):
A=Aw+H
с таким элементом Вейерштрасса (и соответсвующим разложением) ассоциировано два
(аддитивных) гомоморфизма-проекции
Q: A \to A
R: A \to H

(вообще говоря, эти проекции не должны быть непрерывными, потому что проекции с нормой
вообще никак априори не связаны)

Лемма 2.
A -- полное дискретное неархимедово нормированное кольцо, H --
аддитивная подгруппа, w -- элемент Вейерштрасса, такой что Q и R непрерывны.
Пусть некий элемент W\in A такой что (w-W)*Q -- сжимающее отображение.
Тогда W -- тоже элемент Вейерштрасса (по отношению к H)

Док-во леммы 2.
Из непрерывности Q и R изоморфизм
g: A -> A+H
g: x \mapsto (Q(x),R(x))
непрерывен.
Нам нужно доказать, что непрерывный эндоморфизм
f: A+H -> A
f: (a,h) \mapsto aW+h
является изоморфизмом групп.
(w-W)*Q=(g^-1 - f)g=Id-fg -- непрерывный эндоморфизм, который по условию леммы
является сжимающим отображением, значит, по Лемме 1, fg -- автоморфизм. Значит и f автоморфизм.


----

Пусть F -- m-регулярный по t ряд из условия теоремы.

Рассмотрим эндоморфизм кольца K[[x1,x2,...xn,t]]:
h: K[[x1,x2,...xn,t]] -> K[[x1,x2,...xn,t]]
h: f(x1,x2,...,xn,t) \mapsto f(x1^k,x2^k,...,xn^k,t)

где k>m
то есть все переменные, кроме последней, возводим в большую степень k.

Это инъективный морфизм колец: если f(x1^k,x2^k,...,xn^k,t)=0, то f=0

Образ h будет нашим A (c индуцированной из K[[x1,x2,...xn,t]] (x1,x2,...xn,t)-адической нормой,
которую мы в дальнейшем будем называть просто адической), а H -- аддитивная подгруппа A,
состоящая из всех многочленов из K[[x1,x2,...xn]][t]
степени по t меньше m. В качестве элемента Вейерштрасса возьмем w=a_m*t^m (это очевидно
элемент Вейерштрасса, потому что любой ряд однозначно раскладывается в сумму мономов, в которых t
входит в степени меньше m и все остальное). Соответсвующую проекцию обозначим Q, т.е.
f(x1,x2,...xn,t)=g_m(x1,x2,...xn,t)*t^m + g_{m-1}(x1,x2,...xn)*t^m-1 + ... g_0(x1,x2,...xn)

Q:=g_m(x1,x2,...xn)
R:=g_{m-1}(x1,x2,...xn)*t^m-1 + ... g_0(x1,x2,...xn)

обе проекции очевидно непрерывны (если младший ненулевой моном в последовательности рядов f_i имеет все большую
и большую степень, то Q и R имеют все большую и большую кратность в 0, т.к. кратность f -- минимум кратностей Q и R).

Докажем, что h(F) -- тоже элемент Вейерштрасса. Для этого нужно показать (для применения Леммы 2),
что (a_m*t^m - h(F))*Q -- сжимающий эндоморфизм A, то есть для нашей адической нормы, это значит,
что оно увеличивает степень наименьшего ненулевого монома ряда:

пусть f(x1,x2,...,xn,t) \in A, и пусть его наименьший ненулевой моном имеет степень b

Qf(x1,x2,...,xn,t) = g_m(x1,x2,...,xn,t)*t^m
кратность Qf по меньшей мере (b-m)

По условию m-регулярности по t:
a_m*t^m - h(F) = - g(x1^k,...,xn^k,t) + a_m*t^m - a_m*t^m - a_m+1*t^m+1 - ...
где g(x1^k,...,xn^k,t) в каждом мономе есть по крайней мере одна x_i^k
но k>m (по построению), значит кратность (a_m*t^m - h(F)) > m
и кратность (a_m*t^m - h(F))*Q > b-m+m

и, следовательно, по Лемме 2, h(F) -- элемент Вейерштрасса.

----
Пусть P,F как в условии теоремы. Разложим h(P) однозначно в A c помощью элемента Вейерштрасса h(F):

h(P)=h(Q)*h(F)+h(R)

по инъективности P=Q*P+R
F и R выводу теоремы соответствуют, так как h не меняет степень ряда как многочлена от t и регулярность по t.