Finite separable extensions have zero Omega

By [F2] there is $\alpha \in L$ with $L=k(\alpha )$; since $L\mathrm{/}k$ is separable, [F5] makes $\alpha$ separable over $k$, so its minimal polynomial $m\in k[x]$ is monic, irreducible and separable.

By [F4] the separability of the irreducible polynomial $m$ says $m^{\mathrm{\prime }}\mathrm{\ne }0$, where $m^{\mathrm{\prime }}$ is the formal derivative; since $\mathrm{deg}{m}^{\mathrm{\prime }}<\mathrm{deg}m=n$, the minimality statement of [F3] shows $m^{\mathrm{\prime }}(\alpha )\mathrm{\ne }0$: a vanishing of $m^{\mathrm{\prime }}$ at $\alpha$ would force $m\mid m^{\mathrm{\prime }}$ and hence $m^{\mathrm{\prime }}=0$.

Because $\mathrm{d}$ is a $k$-derivation [F1] and $m(\alpha )=0$, applying $\mathrm{d}$ to the relation $m(\alpha )=c_0+c_1\alpha +\cdots +c_n{\alpha }^n$ with $c_n=1$ and using additivity, $k$-linearity and the Leibniz rule gives $0=\mathrm{d}(m(\alpha ))={\sum }_i{c}_i\mathrm{d}({\alpha }^i)=m^{\mathrm{\prime }}(\alpha )\mathrm{d}\alpha$, with $m^{\mathrm{\prime }}(\alpha )\in L$ the value at $\alpha$ of the formal derivative. Since $m^{\mathrm{\prime }}(\alpha )\mathrm{\ne }0$ by step 2.1 and $L$ is a field, $m^{\mathrm{\prime }}(\alpha )$ is invertible in $L$, so $\mathrm{d}\alpha =0$.

It follows that $\mathrm{d}$ vanishes on all of $L$: by [F6] every $f\in L$ equals $p(\alpha )$ for a polynomial $p\in k[x]$, and the Leibniz rule over the expansion of $p(\alpha )$ in powers of $\alpha$ gives $\mathrm{d}p(\alpha )=p^{\mathrm{\prime }}(\alpha )\mathrm{d}\alpha =0$, since $\mathrm{d}\alpha =0$ [F1, step 3.1].

By [F1] the module ${\mathrm{\Omega }}_{L\mathrm{/}k}$ is generated over $L$ by the elements $\mathrm{d}f$ with $f\in L$, and step 4.1 shows that each such generator is zero; hence ${\mathrm{\Omega }}_{L\mathrm{/}k}=0$.