lean_workbook_plus_52723
ProvedProve by AM-GM.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_52723 {a b c d : ℝ} : (a^2 + b^2 + c^2 + d^2)^2 ≥ 16 * a * b * c * d := by sorrySource
Prove by AM-GM.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_52723 {a b c d : ℝ} : (a^2 + b^2 + c^2 + d^2)^2 ≥ 16 * a * b * c * d := by sorry