Definition·D071
Dot product
Multiply corresponding coordinates of two points and add the results.
For
, write
and
, and define
In words
The dot product of two points multiplies their first coordinates together, multiplies their second coordinates together, and adds the two products.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
A function
, well defined by L01 as for D070. Symmetric,
, by commutativity of
on
. Used to define squared distance and orthogonality.