Dimension of a Finite-Dimensional Complex Inner Product Space

Let $V$ together with $\langle\cdot,\cdot\rangle$ be a \reftext{def:complex-inner-product-space-2026a}{complex inner product space} with \reftext{lem:vector-space-basic-identities-2026a}{zero vector} $0_{V}$, and suppose that $V$ is \reftext{def:finite-dimensional-vector-space-2026b}{finite-dimensional} and $V\ne\{0_{V}\}$.

The \textbf{dimension} of $V$, written $\dim V$, is the \reftext{def:natural-numbers-2026a}{natural number} $n$ for which there is an \reftext{def:finite-tuple-power-2026a}{$n$-tuple} in $V$ that is a \reftext{def:finite-basis-2026a}{basis} of $V$; exactly one natural number has this property, by \ref{lem:inner-product-space-basis-size-2026a}.