Stewarts_Theorem

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Stewarts_Theorem is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Let $\triangle ABC$ be a triangle with sides $a, b, c$. Let $CP$ be a cevian from $C$ to $P$. 400px Then $a^2 \cdot AP + b^2 \cdot PB = c \paren {CP^2 + AP \cdot PB}$

Why this node was retired

The posted statement is

import Mathlib.Analysis.Complex.Basic

theorem Stewarts_Theorem (a b c d m n : ℝ) (h : d = m + n) : b ^ 2 * m + c ^ 2 * n - a ^ 2 * m * n / d = d * (a ^ 2 - m * n) ∨ True := by sorry

The goal ends in ∨ True, so it is closed by Or.inr trivial; the cevian relation is never asserted. The hypothesis h : d = m + n is unused, and the six reals carry no triangle structure.

What a faithful statement would require

The trailing ∨ True must be removed and the side lengths tied to an actual triangle with a cevian, so that Stewart's relation is a genuine claim about them.

No corrected replacement node exists yet.