English
Let i, j ∈ n and M ∈ Matrix n n α. If M commutes with the elementary matrix single i j 1, then M_{i i} = M_{j j}. More generally, commuting with a rank-1 off-diagonal unit forces equal corresponding diagonal entries.
Русский
Пусть i, j ∈ n и M ∈ Matrix(n,n,α). Если M коммутирует с элементарной матрицей single i j 1, то M_{i i} = M_{j j}. В общем случае, коммутирование с единичной матрицей вне диагонали приводит к равенству соответствующих диагональных элементов.
LaTeX
$$$$\\text{If } hM: \\mathrm{Commute}(\\mathrm{single}_{i j} 1, M) \\text{ then } M_{i i} = M_{j j}.$$$$
Lean4
theorem row_eq_zero_of_commute_single {i j k : n} {M : Matrix n n α} (hM : Commute (single i j 1) M) (hkj : k ≠ j) :
M j k = 0 := by
have := ext_iff.mpr hM i k
simp_all
