lean_workbook_plus_9863

Open

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

using the fact that $\mathrm{tr}(AB)=\mathrm{tr}(BA)$ . Adding the first two and substracting the third one then gives $2\mathrm{tr}(A)\mathrm{tr}(B)-2\mathrm{tr}(AB)+2\det(A)+2\det(B)-2\det(A+B)=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9863  (A B : Matrix (Fin 2) (Fin 2) ℝ) :
  2 * A.trace * B.trace - 2 * (A * B).trace + 2 * A.det + 2 * B.det - 2 * (A + B).det = 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph