lean_workbook_plus_6193
Provedprove for any real a and b that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6193 (a b : ℝ): a^2 + a * b + b^2 ≥ 3 * (a + b - 1) := by sorry
Source
prove for any real a and b that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_6193 (a b : ℝ): a^2 + a * b + b^2 ≥ 3 * (a + b - 1) := by sorry