ThmDex – An index of mathematical definitions, results, and conjectures.
 ▼ Set of symbols ▼ Alphabet ▼ Deduction system ▼ Theory ▼ Zermelo-Fraenkel set theory ▼ Set ▼ Binary cartesian set product ▼ Binary relation ▼ Map ▼ Operation ▼ N-operation ▼ Binary operation ▼ Enclosed binary operation ▼ Groupoid ▼ Ringoid ▼ Semiring ▼ Ring ▼ Left ring action ▼ Module ▼ Linear combination ▼ Linear map ▼ Multilinear map ▼ Bilinear map ▼ Sesquilinear map ▼ Hermitian map ▼ Hermitian form ▼ Semi-inner product
Definition D34
Inner product

Let $\mathbb{C}$ be the D652: Ring of complex numbers such that
 (i) $V$ is a D29: Vector space over $\mathbb{C}$ (ii) $0_V$ is an D270: Additive identity in $V$
A D4881: Complex function $f : V \times V \to \mathbb{C}$ is an inner product on $V$ over $\mathbb{C}$ if and only if
 (1) $\forall \, x, y, z \in V : f(x + y, z) = f(x, z) + f(y, z)$ (D678: Additive map) (2) $\forall \, x, y, z \in V : f(x, y + z) = f(x, y) + f(x, z)$ (D678: Additive map) (3) $\forall \, x, y \in V : \forall \, r \in \mathbb{C} : f(r x, y) = r f(x, y)$ (D983: Homogeneous map) (4) $\forall \, x, y \in V : \forall \, r \in \mathbb{C} : f(x, r y) = \overline{r} f(x, y)$ (D987: Conjugate homogeneous map) (5) $\forall \, x, y \in V : f(x, y) = \overline{f(y, x)}$ (D729: Conjugate symmetric complex function) (6) $\forall \, x \in V : f(x, x) \geq 0$ (7) $\forall \, x \in V \left( f(x, x) = 0 \quad \implies \quad x = 0_V \right)$
Children
 ▶ Complex Lebesgue inner product
Results
 ▶ Inner product is zero if either argument is zero ▶ Inner product with repeating argument is a real number