lean_workbook_plus_17889

Proved

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

Let $A\in\mathcal{M}_{n}(\mathbb{C})$ s.t. $A$ commutates with $AA^{*}-A^{*}A$ ; then $AA^{*}-A^{*}A$ is a nilpotent matrix. Moreover $AA^{*}-A^{*}A$ is a hermitian matrix and thus is diagonalizable. Conclusion: $AA^{*}=A^{*}A$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17889 {n : ℕ} (A : Matrix (Fin n) (Fin n) ℂ) (h : A * A.conjTranspose - A.conjTranspose * A = 0) : A * A.conjTranspose = A.conjTranspose * A   :=  by sorry

Source

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

View graph