Solution (source code)

= Solution

For a <vector subspace> $U\subseteq V$, its <annihilator of a vector subspace> is
$$
\boxed{U^0=\{\varphi\in V':\varphi(u)=0\text{ for every }u\in U\}}.
$$
Let $\dim U=k$ and $\dim V=n$. Extend a <basis> $u_1,\ldots,u_k$ of $U$ to a <basis> $u_1,\ldots,u_n$ of $V$, and let $\varepsilon^1,\ldots,\varepsilon^n$ be the <dual basis>. Every <linear functional> has the unique expression $\varphi=\sum_{j=1}^n\varphi(u_j)\varepsilon^j$. It belongs to $U^0$ precisely when its first $k$ coefficients vanish. Consequently
$$
U^0=\operatorname{span}\{\varepsilon^{k+1},\ldots,\varepsilon^n\},\qquad
\boxed{\dim U+\dim U^0=\dim V}.
$$
The listed <dual basis> elements are <linearly independent>, so counting them proves the formula, including $U=0$ and $U=V$.