Prove2Me

lean_workbook_plus_68415

Proved

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

(2017⋅2018−2016⋅2019)x2−(2017⋅2018−2016⋅2019)4035x=0(2017\cdot 2018-2016\cdot 2019)x^2-(2017\cdot 2018-2016\cdot 2019)4035x=0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_68415 (x : ℝ) (hx: x ≠ 0) : (2017 * 2018 - 2016 * 2019) * x ^ 2 - (2017 * 2018 - 2016 * 2019) * 4035 * x = 0 ↔ x = 0 ∨ x = 4035   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph