\begin{definition}[Definition:Inner Product]
Let $\C$ be the field of complex numbers.
Let $\GF$ be a subfield of $\C$.
Let $V$ be a vector space over $\GF$.
An '''inner product''' is a mapping $\innerprod \cdot \cdot: V \times V \to \GF$ that satisfies the following properties:
{{begin-axiom}}
{{axiom | n = 1
        | lc= Conjugate Symmetry
        | q = \forall x, y \in V
        | m = \quad \innerprod x y = \overline {\innerprod y x}
}}
{{axiom | n = 2
        | lc= Linearity in first argument
        | q = \forall x, y \in V, \forall a \in \GF
        | m = \quad \innerprod {a x + y} z = a \innerprod x z + \innerprod y z
}}
{{axiom | n = 3
        | lc= Non-Negative Definiteness
        | q = \forall x \in V
        | m = \quad \innerprod x x \in \R_{\ge 0}
}}
{{axiom | n = 4
        | lc= Positiveness
        | q = \forall x \in V
        | m = \quad \innerprod x x = 0 \implies x = \mathbf 0_V
}}
{{end-axiom}}
That is, an inner product is a semi-inner product with the additional condition $(4)$.
If $\GF$ is a subfield of the field of real numbers $\R$, it follows from Complex Number equals Conjugate iff Wholly Real that $\overline {\innerprod y x} = \innerprod y x$ for all $x, y \in V$.
Then $(1)$ above may be replaced by:
{{begin-axiom}}
{{axiom | n = 1'
        | lc= Symmetry
        | q = \forall x, y \in V
        | m = \innerprod x y = \innerprod y x
}}
{{end-axiom}}
\end{definition}