English
Let A be m × n, i ∈ m, r : n → α, e : m ≃ l, f : n ≃ o. Then reindex e f applied to A.updateRow i r equals updateRow on the reindexed A at e i with row r composed with f.symm: reindex e f (A.updateRow i r) = updateRow (reindex e f A) (e i) (λ k, r (f.symm k)).
Русский
Пусть A — матрица размером m×n, i ∈ m, r : n → α, e : m ≃ l, f : n ≃ o. Тогда повторная индексация матрицы после обновления строки равна обновлению в новой индексации: reindex e f (A.updateRow i r) = updateRow (reindex e f A) (e i) (λ k, r (f.symm k)).
LaTeX
$$$$ reindex e f (A.updateRow i r) = updateRow (reindex e f A) (e i) (\lambda k, r (f.symm k)) $$$$
Lean4
theorem reindex_updateRow [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : m) (r : n → α) (e : m ≃ l)
(f : n ≃ o) : reindex e f (A.updateRow i r) = updateRow (reindex e f A) (e i) fun i => r (f.symm i) :=
submatrix_updateRow_equiv _ _ _ _ _
