Solution (source code)

= Solution

The <annihilator of a vector subspace> $W\leq V^*$ is
$$
\boxed{W^\circ=\{L\in V^{**}:L(\phi)=0\text{ for every }\phi\in W\}.}
$$
If $\dim W=k$, extend a <basis> of $W$ to one of $V^*$. In the resulting <dual basis> of $V^{**}$, the last $n-k$ coordinate functionals span $W^\circ$. Hence $\boxed{\dim W+\dim W^\circ=n}$.

The <bidual evaluation map> $j:V\to V^{**}$ is $j(x)(\phi)=\phi(x)$. It is a <linear isomorphism> in finite dimension. Its inverse image of the annihilator is
$$
\boxed{j^{-1}(W^\circ)=\{x\in V:\phi(x)=0\text{ for every }\phi\in W\}.}
$$
This identification uses evaluation only; no choice of <inner product> is involved.