Length_of_Angle_Bisector
Disprovedlength-of-angle-bisectorproofwikitriangles
Let be a triangle. Let be the angle bisector of in . 300px Let be the length of . Then is given by where , , and are the sides opposite , and respectively.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Length_of_Angle_Bisector (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : ∃ t : ℝ, t ^ 2 = b * c * ((b + c) ^ 2 - a ^ 2) / (b + c) ^ 2 := by sorry
Source