Commit 2025-09-23 16:16 11471b6c

View on Github →

chore(Geometry/Euclidean/SignedDist): use normalize (#29897) This PR uses the new NormedSpace.normalize in signedDist. It also fills in some missing API.

Estimated changes

modified theorem signedDist_apply
modified theorem signedDist_apply_apply
modified theorem signedDist_apply_linear
modified theorem signedDist_linear_apply
added theorem signedDist_smul_of_neg
added theorem signedDist_smul_of_pos
modified theorem signedDist_vadd_left
modified theorem signedDist_vadd_right