Commit 2025-09-01 07:30 7ad4d9be

feat(Geometry/Euclidean/SignedDist): signedDist between two points (#27260) original PR: #24245 This PR defines signedDist, the signed distance between two points. It also redefines signedInfDist so that it uses signedDist. The motivation is to use this in IMO2020Q6. Additionally this definition will be useful for properly reasoning about the power of a point #mathlib4 > Signed distance between points some comments:

• should signedDistLinear be private?
• I'm not too happy about the hypothesis in signedDist_congr (h : ∃ r > (0 : ℝ), r • v = w). This relationship between v and w is a symmetric one that should have some API around it, similar to SameRay. It could also be spelled as (ℝ≥0 ∙ v) = ℝ≥0 ∙ w