lean_workbook_plus_2024
ProvedBy AM-GM
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2024 (a : ℝ) : a^2 + 1 / 9 ≥ 2 / 3 * a := by sorry
Source
By AM-GM
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_2024 (a : ℝ) : a^2 + 1 / 9 ≥ 2 / 3 * a := by sorry