lean_workbook_plus_2271
OpenProve that the determinant of the matrix is equal to without expanding the determinant.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2271 (x y : ℂ) : Matrix.det (![![y, x, x+y],![x+y, y, x],![x, x+y, y]]) = 2 * (x^3 + y^3) := by sorry
Source