lean_workbook_plus_18973
ProvedCase 2:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_18973 (p q : ℤ) (h₁ : (p : ℝ)^2 - 4 * q = (abs p - 2)^2) : q = abs p - 1 := by sorry
Source
Case 2:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_18973 (p q : ℤ) (h₁ : (p : ℝ)^2 - 4 * q = (abs p - 2)^2) : q = abs p - 1 := by sorry