lean_workbook_plus_30281

Proved

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

Write the system in the form\n $\frac{b^2-2ab}{a^2-2ab}=\frac{117}{165}$ and from here we get\n ${ \frac{\frac{b}{a}-2}{\frac{a}{b}-2}}=\frac{117}{165}$ . By setting $z=\frac{a}{b}$ you will get a quadratic equation.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30281  (a b : ℝ)
  (h₀ : a ≠ 0 ∧ b ≠ 0)
  (h₁ : a ≠ b)
  (h₂ : (b^2 - 2 * a * b) / (a^2 - 2 * a * b) = 117 / 165) :
  (b / a - 2) / (a / b - 2) = 117 / 165   :=  by sorry

Source

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

View graph