updateCol_comm — Mathlib

English

Updating two different columns in a matrix commutes: (A.updateCol j x).updateCol j' y = (A.updateCol j' y).updateCol j x.

Русский

Обновление двух разных столбцов матрицы коммутирует: (A.updateCol j x).updateCol j' y = (A.updateCol j' y).updateCol j x.

LaTeX

$$$$ (A.updateCol j x).updateCol j' y = (A.updateCol j' y).updateCol j x $$$$

Lean4

theorem updateCol_comm [DecidableEq n] (A : Matrix m n α) {j j' : n} (h : j ≠ j') (x y : m → α) :
    (A.updateCol j x).updateCol j' y = (A.updateCol j' y).updateCol j x := by
  simpa only [updateRow_transpose] using congr_arg transpose <| updateRow_comm Aᵀ h x y

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