lean_workbook_plus_15720
Disprovedprove
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15720 : ∀ a b c : ℝ, (a+b)*(b+c) ≥ (Real.sqrt (b*c) + Real.sqrt (b*a))^2 := by sorry
Source
prove
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_15720 : ∀ a b c : ℝ, (a+b)*(b+c) ≥ (Real.sqrt (b*c) + Real.sqrt (b*a))^2 := by sorry