Definition·D072
Squared distance
The dot product of a point-difference with itself: the squared length of the segment between two points.
In words
The squared distance between two points is the dot product of their difference with itself.
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
Writing
,
, this unwinds to
, the sum of the squares of the coordinate differences. No square root is needed to state the Pythagorean theorem, so this library works with squared distance rather than constructing the reals.