Linearly disjoint field extensions (source code)

= Linearly disjoint field extensions
{wiki=Linearly_disjoint}

Finite extensions $L_1/K$ and $L_2/K$ are linearly disjoint when products of basis elements form a basis of their compositum. In particular,
$$
[L_1L_2:K]=[L_1:K][L_2:K].
$$
Extensions of coprime finite degrees are linearly disjoint.