Prove2Me

lean_workbook_plus_82549

Proved

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

proofwiki

Given α⋅β+β⋅γ+γ⋅α=0\alpha\cdot\beta + \beta \cdot \gamma + \gamma\cdot \alpha = 0 and α⋅β⋅γ=1\alpha\cdot\beta\cdot \gamma=1, prove that 1γ=1−α+1−β\frac{1}{\gamma}=\frac{1}{-\alpha}+\frac{1}{-\beta}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_82549 (α β γ : ℝ) (h₁ : α * β + β * γ + γ * α = 0) (h₂ : α * β * γ = 1) : 1 / γ = 1 / -α + 1 / -β   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph