Trace and determinant of a sum of two-by-two matrices

Proved

WorkbookRestored.plus_9863

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

lean-workbookrestored-importssource-checked

For real two-by-two matrices $A,B$ ,

2\operatorname{tr}(A)\operatorname{tr}(B)-2\operatorname{tr}(AB)+2\det A+2\det B-2\det(A+B)=0.

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_9863 (Apache-2.0).

Preamble

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

Formal statement

theorem WorkbookRestored.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/blob/main/lean_workbook.json, row lean_workbook_plus_9863; original Prove2Me node d95afd95-555f-4eeb-adaf-3bc5da7f06b6; Apache-2.0

View graph