lean_workbook_plus_39724
ProvedGiven two natural numbers and , prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_39724 (a b : ℕ) : Real.sqrt (a * b) ≤ (a + b) / 2 := by sorry
Source
Given two natural numbers and , prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_39724 (a b : ℕ) : Real.sqrt (a * b) ≤ (a + b) / 2 := by sorry