Corollary 3

— Let K be a field of characteristic $p \neq 0$ and L a finitely generated extension of K of transcendence degree s. If $[K : K^p]$ is finite, the same is true of $[L : L^p]$ and we have $[L : L^p] = p^s$. $[K : K^p]$. Let P be the prime subfield of K. If $[K : K^p]$ is finite, then the vector space $\Omega_P(K) = \Omega_{K^p}(K)$ is of finite dimension m over K, and we have $[K : K^p] = p^m$ (V, p. 103, Th. 2); the vector space $\Omega_P(K) \otimes_K L$ is then of finite dimension m over L. Further, since K is of finite degree over $K^p$, the field $K(L^p)$ is of finite degree over $K^p(L^p) = L^p$; since the field L is a finitely generated extension of K and is algebraic over $K(L^p)$, it is an extension of finite degree of $K(L^p)$ (V, p. 18, Th. 2); we thus conclude that L is of finite degree over $L^p$ (V, p. 10, Th. 1). Then $\Omega_P(L)$ is a vector space of finite dimension n over L and we have $[L : L^p] = p^n$ (V, p. 103, Th. 2). By Lemma 1 (V, p. 132) the L-linear mapping $\alpha : \Omega_P(K) \otimes_K L \to \Omega_P(L)$ therefore has index $n - m$, whence $n - m = s$ by Th. 4 (V, p. 133) and $p^n = p^s \cdot p^m$.