Lean-Workbook Plus 69206: A two-by-two commutator determinant identity

Proved

WorkbookRestored.plus_69206

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For real $2\times2$ matrices $A,B$ , $\det(AB-BA)+\det(AB+BA)=4\det(AB)$ .

Source: Lean-Workbook row lean_workbook_plus_69206 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Formal statement

theorem WorkbookRestored.plus_69206  (A B : Matrix (Fin 2) (Fin 2) ℝ) :
  (A * B - B * A).det + (A * B + B * A).det = 4 * (A * B).det   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_69206; immutable original Prove2Me node 79d41c30-89e9-4bbc-a234-5443f3fe720a

View graph