lean_workbook_plus_51658
DisprovedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_51658 : ∀ a b : ℝ, Real.sqrt (a * b) ≤ (Real.sqrt 3 * a + b / Real.sqrt 3) / 2 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_51658 : ∀ a b : ℝ, Real.sqrt (a * b) ≤ (Real.sqrt 3 * a + b / Real.sqrt 3) / 2 := by sorry