Tower law for field extensions (source code)

= Tower law for field extensions

For finite extensions $K\subseteq E\subseteq L$, the degrees multiply:
$$
[L:K]=[L:E][E:K].
$$
If $(u_i)$ is a $K$-basis of $E$ and $(v_j)$ is an $E$-basis of $L$, then the products $(u_iv_j)$ form a $K$-basis of $L$: spanning follows by expanding first over $E$ and then over $K$, while $K$-linear independence follows by grouping coefficients of each $v_j$ and using both basis properties.