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
Formulation 3
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)$
Also known as
Complex inner product
Children
▶ D781: Complex Lebesgue inner product
Results
▶ R1372: Inner product is zero if either argument is zero
▶ R4705: Inner product with repeating argument is a real number