lean_workbook_plus_39820

Proved

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

Solve the system of equations $a = \sqrt{ab}$ and $b = \frac{a+b}{2}$ to show that $a = b$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39820 (a b : ℝ) (h₁ : a = Real.sqrt (a * b)) (h₂ : b = (a + b) / 2) : a = b   :=  by sorry

Source