lean_workbook_plus_16006

Proved

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

Prove that $\frac{bc}{b^2+c^2}=\frac{1}{\frac bc+\frac cb}=\frac{1}{2Re\; \frac bc}\in \mathbb{R}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16006 (b c : ℂ) :
  (b * c) / (b * b + c * c) = 1 / (b / c + c / b)   :=  by sorry

Source