updateCol_reindex — Mathlib

English

Updating a column after reindexing a matrix equals reindexing after updating the corresponding column.

Русский

Обновление столбца после перестановки строк и столбцов равнозначно перестановке после обновления соответствующего столбца.

LaTeX

$$$\bigl(\mathrm{updateCol}(\mathrm{reindex}\ e\ f\ A)\bigr)\, j\, c = \mathrm{reindex}\ e\ f\bigl(A.\mathrm{updateCol}(\mathrm{f^{-1}}(j))\bigl(\lambda i, c(i)\bigr)\bigr)$$$

Lean4

theorem updateCol_reindex [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : o) (c : l → α) (e : m ≃ l)
    (f : n ≃ o) : updateCol (reindex e f A) j c = reindex e f (A.updateCol (f.symm j) fun i => c (e i)) :=
  updateCol_submatrix_equiv _ _ _ _ _

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