lean_workbook_plus_63556

Proved

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

Try to prove that the cubic $\frac{x^3}{3}+\frac{x^2}{2}+x$ is injective.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63556 (x y : ℝ) (h : x^3 / 3 + x^2 / 2 + x = y^3 / 3 + y^2 / 2 + y) : x = y   :=  by sorry

Source