Поле разложения степени n

[Dedekind]

Пусть $[K:F] = n$, где $K$ - поле разложения некоторого полинома над $F$. Тогда $K$ - поле разложения над $F$ любого неприводимого полинома степени $n$ в $F[x]$, который имеет корень в $K$. Тут считается, что $\operatorname{char}(F) = 0$.

Правильны ли такие рассуждения?
Ранее было доказано, что при таких условиях, все корни любого неприводимого полинома $p(x)\in F[x]$ содержатся в $K$. То есть, осталось доказать только минимальность. Пусть $F(a_1, ... , a_n)\subseteq K$ - поле разложения $p(x)$, причем $[F(a_1, ... , a_n):F] \le n$. Поскольку $p(x)$ неприводим, то он является минимальным полиномом для $a_1$, а следовательно размерность $F(a_1)$ равна $n$. Поскольку $F(a_1) \subseteq F(a_1, ... , a_n)$, то $[F(a_1, ... , a_n):F] \ge n$. Следовательно, $[F(a_1, ... , a_n):F] = n$ и $F(a_1, ... , a_n) = K$.

[Gagarin1968]

Dedekind
Да, похоже, всё безупречно.
Всё как по учебнику: проверка базовых условий (сепарабельности), оценка степени расширения сверху, оценка степени расширения снизу и окончательный вывод на основе совпадения размерностей.

[Dedekind]

Gagarin1968
Спасибо!