lean_workbook_plus_7494
ProvedLet be reals such that . Prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7494 (a b : ℝ) (h : (a + b) * (a + 4 * b) = 9) : a * b ≤ 1 := by sorry
Source
Let be reals such that . Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_7494 (a b : ℝ) (h : (a + b) * (a + 4 * b) = 9) : a * b ≤ 1 := by sorry