mathlib3

ea9c24f6 - feat(geometry/euclidean/basic): second intersection of a line and a sphere (#17843)

feat(geometry/euclidean/basic): second intersection of a line and a sphere (#17843) A very common geometrical construction is taking the second intersection of a line and a sphere (where one intersection point is given); we already have a lemma `dist_smul_vadd_eq_dist` that gives a characterization of that point. Add an explicit definition `sphere.second_inter` for this construction and associated API.