lean_workbook_plus_5168

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_5168 (a b c d : ℝ) (hab : a + b + c + d = 0) : (a * b * c + b * c * d + c * d * a + d * a * b) ^ 2 = |(b * c - a * d) * (c * a - b * d) * (a * b - c * d)|   :=  by sorry