Let XX be a over R\mathbb{R} or C\mathbb{C}, and let f:XKf:X\to\mathbb{K} be a nonzero linear functional with kerf\ker f.

Proposition:

codim(kerf)=1.\operatorname{codim}(\ker f)=1.
Remarks

Context: The kernel of a nonzero functional is a codimension-one subspace, and translates of such kernels are precisely in real vector spaces; see .