Commit 2026-10-17 17:39 f5517aa5
View on Github →feat(Geometry/Euclidean/Angle/Incenter): distance from second intersection with circumcircle (#32294) Add the following lemma: given a triangle ABC, suppose an angle bisector from A through the incenter or excenter I meets the circumcircle again at X (including the case of an external bisector at A tangent to the circle, in which case X = A). Then XB = XI (= XC, by applying this lemma again). This is a standard configuration: https://en.wikipedia.org/wiki/Incenter%E2%80%93excenter_lemma