WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Non-Euclidean geometry

Revision #2043 → #2482 · back to history

modifiedModulus equals squared Euclidean distancee9d425796c79
FieldFrom #2043To #2482
note`Complex.normSq z = z.re^2 + z.im^2` is the squared Euclidean distance from z to 0; the Wikipedia 'modulus' here means z·z* (= normSq).`Complex.normSq z = z.re^2 + z.im^2` is the squared Euclidean distance from z to 0; the Wikipedia 'modulus' here means z·z* (= normSq). Status upgraded to formalized to match the exact match_kind.
provenanceaiai-moderated
statuspartialformalized
addedRiemannian geometryda6b769c988f
addedCurvature tensor0d485960dca3
addedAntipodal points on a sphere9c0d46683e55
addedHyperbolic planeb059414c00ab