lean_workbook_plus_33215

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

If $x_1x_2=bc$ and $x_2x_3=ac$ , then $x_2(x_1-x_3)=c(b-a)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_33215 (a b c x₁ x₂ x₃ : ℂ) (h₁ : x₁ * x₂ = b * c) (h₂ : x₂ * x₃ = a * c) : x₂ * (x₁ - x₃) = c * (b - a)   :=  by sorry

Source