# [isabelle] New in the AFP: Stewartâs Theorem and Apolloniusâ Theorem (by Lukas Bulwahn)

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] New in the AFP: Stewartâs Theorem and Apolloniusâ Theorem (by Lukas Bulwahn)
*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>
*Date*: Tue, 1 Aug 2017 14:55:02 +0000
*Accept-language*: de-DE, de-AT, en-US
*Thread-index*: AQHTCtYnesM0z2MvyU2cYuPMXzgLWw==
*Thread-topic*: New in the AFP: Stewartâs Theorem and Apolloniusâ Theorem (by Lukas Bulwahn)

Stewartâs Theorem and Apolloniusâ Theorem
by Lukas Bulwahn
This entry formalizes the two geometric theorems, Stewart's and
Apollonius' theorem. Stewart's Theorem relates the length of
a triangle's cevian to the lengths of the triangle's two
sides. Apollonius' Theorem is a specialisation of Stewart's
theorem, restricting the cevian to be the median. The proof applies
the law of cosines, some basic geometric facts about triangles and
then simply transforms the terms algebraically to yield the
conjectured relation. The formalization in Isabelle can closely follow
the informal proofs described in the Wikipedia articles of those two
theorems.
https://www.isa-afp.org/entries/Stewart_Apollonius.shtml
Enjoy,
RenÃ

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*