lean_workbook_plus_69206

Open

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

Prove (3): $det(AB-BA)+det(AB+BA)=4det(AB)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_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