diag_eq_of_commute_single — Mathlib

English

If a matrix M commutes with every non-diagonal single, then M is a scalar matrix; equivalently, M lies in the range of the scalar map.

Русский

Если матрица M коммутирует с каждой ненулевой единичной матрицей вне диагонали, то она скалярная; эквивалентно M принадлежит образу отображения скаляра.

LaTeX

$$$$M \\in \\mathrm{Set.range}(\\mathrm{scalar}\\ n) \\quad \\text{iff} \\quad \\forall i \\neq j,\\; [\\mathrm{Commute}(\\mathrm{single}_{i j} 1, M)].$$$$

Lean4

theorem diag_eq_of_commute_single {i j : n} {M : Matrix n n α} (hM : Commute (single i j 1) M) : M i i = M j j :=
  by
  have := ext_iff.mpr hM i j
  simp_all

Похожие утверждения