lean_workbook_plus_13938

Proved

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

$= \frac{1}{\sqrt{97}}(16(\frac{a}{4} + \frac{1}{9a} + \frac{b}{4} + \frac{1}{9b} + \frac{c}{4} + \frac{1}{9c}) + 65(\frac{1}{9a} + \frac{1}{9b} + \frac{1}{9c}))$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13938 (a b c : ℝ) : (1 / Real.sqrt 97) * (16 * (a / 4 + b / 4 + c / 4) + 65 * (1 / 9 * a + 1 / 9 * b + 1 / 9 * c)) = (1 / Real.sqrt 97) * (16 * (a / 4 + b / 4 + c / 4) + 65 * (1 / 9 * a + 1 / 9 * b + 1 / 9 * c))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph