lean_workbook_plus_24261
DisprovedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_24261 : ∀ p q : ℝ, p^2 - 6 * p + q^2 - 2 * q + 6 ≥ (p - 3)^2 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_24261 : ∀ p q : ℝ, p^2 - 6 * p + q^2 - 2 * q + 6 ≥ (p - 3)^2 := by sorry