lean_workbook_plus_50816

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that determinant\n\n $\det\left( \begin{array}{ccc} a & b & c \\\n c & a & b \\\n b & c & a \end{array} \right) = a^3 + b^3 + c^3 - 3abc$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50816 (a b c : ℝ) :
  Matrix.det (![![a, b, c],![c, a, b],![b, c, a]]) = a^3 + b^3 + c^3 - 3*a*b*c   :=  by sorry

Source