`BookProof.ChapterAbelianVonNeumannFinite.commutes_diagonal_iff` (e : n → ℂ) (he : Function.Injective e) (M : Matrix n n ℂ) : M * diagonal e = diagonal e * M ↔ ∃ d : n → ℂ, M = dia

Proved

BookProof.ChapterAbelianVonNeumannFinite.commutes_diagonal_iff

by leonardopedro · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterAbelianVonNeumannFinite.

BookProof.ChapterAbelianVonNeumannFinite.commutes_diagonal_iff (e : n → ℂ) (he : Function.Injective e) (M : Matrix n n ℂ) : M * diagonal e = diagonal e * M ↔ ∃ d : n → ℂ, M = diagonal d

Formalization note: Lean 4 identifier BookProof.ChapterAbelianVonNeumannFinite.commutes_diagonal_iff.

Preamble

-- Generated from ChapterAbelianVonNeumannFinite.lean — theorem BookProof.ChapterAbelianVonNeumannFinite.commutes_diagonal_iff
import Mathlib
import Definitions.Def_ChapterAbelianVonNeumannFinite
open BookProof.ChapterAbelianVonNeumannFinite


open Matrix


variable {n : Type*} [Fintype n] [DecidableEq n]

Formal statement

theorem BookProof.ChapterAbelianVonNeumannFinite.commutes_diagonal_iff (e : n → ℂ) (he : Function.Injective e) (M : Matrix n n ℂ) :
    M * diagonal e = diagonal e * M ↔ ∃ d : n → ℂ, M = diagonal d := by sorry

View graph