lean_workbook_plus_15822
ProvedGiven that and , prove that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15822 (a b : ℝ) (hab : a > 0 ∧ b > 0) : (a + b) ^ 2 ≥ 4 * a * b := by sorry
Source
Given that and , prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_15822 (a b : ℝ) (hab : a > 0 ∧ b > 0) : (a + b) ^ 2 ≥ 4 * a * b := by sorry