lean_workbook_plus_14321
ProvedUsing AM-GM inequality, prove that if , then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14321 (a b : ℝ) (h : a + b = 4) : a * b ≤ 4 := by sorry
Source
Using AM-GM inequality, prove that if , then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_14321 (a b : ℝ) (h : a + b = 4) : a * b ≤ 4 := by sorry