lean_workbook_plus_18218
ProvedProve .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_18218 (a b c d : ℝ) : (a^2+c^2)*(b^2+d^2)*(c^2+d^2+a^2+b^2) ≥ (a*b*c+b*c*d+c*d*a+d*a*b)^2 := by sorry
Source
Prove .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_18218 (a b c d : ℝ) : (a^2+c^2)*(b^2+d^2)*(c^2+d^2+a^2+b^2) ≥ (a*b*c+b*c*d+c*d*a+d*a*b)^2 := by sorry