lean_workbook_plus_21514

Proved

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

Verify the equality $\frac{1}{a + bi} = \frac{a - bi}{a^2 + b^2}$ without calculation.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_21514 : ∀ a b : ℝ, (a - b * Complex.I) / (a ^ 2 + b ^ 2) = (a + b * Complex.I)⁻¹   :=  by sorry

Source