col_eq_zero_of_commute_single — Mathlib

English

If M commutes with single i j 1, then M_{j k} = 0 for all k ≠ j; equivalently, the j-th column is zero except possibly on the diagonal entry.

Русский

Если M коммутирует с single i j 1, то M_{j k} = 0 для всех k ≠ j; иначе говоря, j-й столбец обнуляется вне диагонали.

LaTeX

$$$$\\text{If } hM: \\mathrm{Commute}(\\mathrm{single}_{i j} 1, M) \\text{ and } hkj: k \\neq j, \\text{ then } M_{j k} = 0.$$$$

Lean4

theorem col_eq_zero_of_commute_single {i j k : n} {M : Matrix n n α} (hM : Commute (single i j 1) M) (hki : k ≠ i) :
    M k i = 0 := by
  have := ext_iff.mpr hM k j
  simp_all

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