$K^{1/p}\otimes_K K[[x]] \subseteq K^{1/p}[[x]]$ is a flat extension

35 Views Asked by At

I'm reading the proof of Kunz theorem, the "easy" part that says a ring $R$ of prime characteristic $p$ being regular implies that the Frobenius map $R\to R, r\mapsto r^p$ is flat. There is a detail saying

"$K^{1/p}\otimes_K K[[x]] \subseteq K^{1/p}[[x]]$ is a flat extension because completion is flat."

Here $K$ is a field of characteristic $p$ and $K^{1/p} $ is the ring containing all the $p$-roots of elements in $K$.

By definition, I can prove that this is indeed an inclusion. But that's it. Why is this extension is exactly the completion?