English
Let A be a matrix m × n, i ∈ l, r : o → α, e : m ≃ l, f : n ≃ o. Then updating the i-th row after reindexing equals reindexing the updateRow of A with i transported by e and r transported by f: updateRow (reindex e f A) i r = reindex e f (A.updateRow (e.symm i) (λ j, r (f j))).
Русский
Пусть A — матрица размером m×n, i ∈ l, r : o → α, e : m ≃ l, f : n ≃ o. Тогда обновление i-й строки после повторной индексации равно повторной индексации обновления строки A с i, перенесенным через e, и r, перенесенным через f: updateRow (reindex e f A) i r = reindex e f (A.updateRow (e.symm i) (λ j, r (f j))).
LaTeX
$$$$ updateRow (reindex e f A) i r = reindex e f (A.updateRow (e.symm i) (\lambda j, r (f j))) $$$$
Lean4
theorem updateRow_reindex [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α) (e : m ≃ l)
(f : n ≃ o) : updateRow (reindex e f A) i r = reindex e f (A.updateRow (e.symm i) fun j => r (f j)) :=
updateRow_submatrix_equiv _ _ _ _ _
