I have recently learned the following theorem.
Let $E$ be a field and let $H$ be a finite group of automorphisms of $E.$ Then $(E:E^H)=\operatorname{card}(H),$ where $E^H$ is the subfield of elements which are fixed by all automorphisms in $H.$
The proof depends on the finiteness of $H$ because it uses linear equations in $n$ (and also $n+1$) variables, where $n=\operatorname{card}(H).$ Is the theorem still true if we drop this assumption? If it is, is it possible to give a proof of the general case without distinguishing the cases of $H$ finite and $H$ infinite?
Re Pierre-Yves Gaillard's answer
$(1)$ Why is the Galois group $G=\operatorname{Aut}(K/F_p)$ uncountable?
Clearly, $\operatorname{card}(G)\leq \operatorname{card}(K)^{\operatorname{card}(K)}=\aleph_0^{\aleph_0}=\mathfrak c.$ I'm having trouble with the other inequality. Here's a slightly "more accurate" way of bounding $\operatorname{card}(G)$ from above.
We have $K=\bigcup_{n=1}^\infty F_{p^n}.$ Therefore, in particular $K$ is countable as a union of countably many finite sets. Let $\alpha\in G$ and $x\in K.$ Then there is $k\in \mathbb N$ such that $x^{p^k}-x=0$ and so $(\alpha(x))^{p^k}-\alpha(x)=0.$ So every element $x\in F_{p^k}$ is mapped to one of the $p^k$ elements of $F_{p^k}.$ So to define an automorphism we have to make countably many finite choices, which again means that $\operatorname{card}(G)\leq\mathfrak c.$ But it doesn't prove that there is equality because certainly not all such choices are OK. How can this be improved?
$(2)$ I understand that you're using the following formula. $K^G=F_p.$ For this I would have to show that if $\xi\in K\setminus F_p$ then there exists $\alpha\in G$ such that $\alpha(x)\neq x.$ This looks very true. Let $f$ be the minimal polynomial of $\xi$ over $F_p.$ Its degree is greater than $1.$ Suppose it has no roots in $K$ other than $\xi.$ Then $\xi$ is a multiple root of $f$ and so f'(\xi)=0. But then f'=0 because \deg(f')<\deg(f). So $f$ must be of the form $f(x)=a_nx^{pn}+a_{n-1}x^{p(n-1)}+\ldots+a_1x^p+a_0.$ There is $k\in\mathbb N$ such that $\xi\in F_{p^k}.$ But $\phi(x)=x^p$ is an automorphism of $F_{p^k}$ and therefore so is $\phi^{-1}$. So since $a_n(\xi^p)^n+a_{n-1}(\xi^p)^{n-1}+\ldots+a_1\xi^p+a_0=0,$ we also have $g(\xi):=a_n\xi^n+a_{n-1}\xi^{n-1}+\ldots+a_1\xi+a_0=0.$ Now $\deg f=pn$ and $\deg g=n$ and both have $\xi$ as their zero. Therefore $n$ must be zero, because otherwise $pn>n.$ But then $\deg f=pn=0,$ a contradiction.
So $f$ has another root $\eta\neq\xi.$ We should be able to construct an automorphism of $K$ sending $\xi$ to $\eta.$ I think there is such an automorphism of $F_{p^n}$ by a theorem about splitting fields. Why can I extend it to $K?$