Solution (source code)

= Solution

A <field extension> $K/F$ is finite when $K$, regarded as a <vector space> over $F$, has finite <dimension>. Its <degree of a field extension> is
$$
\boxed{[K:F]=\dim_F K}.
$$
Thus a finite <basis> $u_1,\ldots,u_m$ means that every $k\in K$ is uniquely expressible as $\sum_i c_i u_i$ with coefficients $c_i\in F$.