Prove2Me

lean_workbook_plus_3299

Proved

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

k=c−ab−a=−c−aa−b  ⟹  1k=−a−bc−a⋯(2)k = \frac{c-a}{b-a} = -\frac{c-a}{a-b} \implies \frac{1}k =- \frac{a-b}{c-a}\cdots (2)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3299 (a b c k : ℝ) : (k = (c - a) / (b - a) ∧ k = -((c - a) / (a - b))) → 1 / k = -(a - b) / (c - a)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph