lean_workbook_plus_9439

Proved

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

Let $r,p$ be real numbers. Prove that if $2r + p, r^2 + 2rp, r^2p$ are rational, then $r$ and $p$ are rational.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9439 {r p : ℝ} : (∃ q, 2 * r + p = q) ∧ (∃ q, r ^ 2 + 2 * r * p = q) ∧ (∃ q, r ^ 2 * p = q) → ∃ q, r = q ∧ ∃ q, p = q   :=  by sorry

Source

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

View graph