Commit 2026-10-17 12:17 d49d3da0
View on Github →feat(Geometry/Euclidean): dist with affineCombination on one side (#44102)
Supplementing existing theorems about dist affineCombination affineCombination, this one calculates dist affineCombination Q with affineCombination only on one side.
I intentionally did not follow the existing style in the file, and wrote x ^ 2 instead of x * x. The latter results in unnecessary duplication and is not ring-normal form. The x * x style seems to appear a lot in old Euclidean geometry code. We should refactor them but that can be later.