Ceva's theorem

Ceva's theorem.

Let $t$ be a triangle with vertices $A_0, A_1, A_2$, and for each $i$ let $P_i$ be a point on the line through the other two vertices $A_{i+1}, A_{i+2}$. If the three cevians $A_iP_i$ are concurrent — all passing through a common point $p'$ — then

Each cevian cuts the opposite side in some ratio; the theorem says concurrency forces the three ratios to multiply to one. It is the clean criterion for three lines through the vertices to meet, and it immediately gives the concurrency of the medians (all ratios $1$), the angle bisectors (via the bisector length formula), and the altitudes. The converse holds too, which is how the standard triangle centres are usually proved to exist.

Giovanni Ceva published it in De lineis rectis (1678), though it was known to al-Mu'taman ibn Hud in 11th-century Zaragoza. It is the projective dual companion to Menelaus' theorem, where collinearity of three points on the sides gives product $-1$ in signed ratios.

Formalization note. Indices are in Fin 3 so i + 1, i + 2 wrap cyclically; line[𝕜, x, y] is the affine span of two points, and the hypothesis hp0 rules out the degenerate zero denominator. Working with unsigned distances is why the product is $+1$ rather than a signed $\pm 1$. The result is Mathlib's Affine.Triangle.prod_dist_div_dist_eq_one_of_mem_line_of_mem_line.