Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-21 06:49 ea9c24f6

View on Github →

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.

Estimated changes