English
Let A be an m × n matrix over α, i ∈ m, r : n → α, e : l ≃ m, f : o ≃ n. Then updating the i-th row of A by r and then taking the submatrix via e and f is the same as taking the submatrix of A via e and f and then updating the row e.symm i by the row r transported along f; i.e., (A.updateRow i r).submatrix e f = updateRow (A.submatrix e f) (e.symm i) (λ k, r (f k)).
Русский
Пусть A — матрица размера m на n над полем α, i ∈ {1,...,m}, r : {1,...,n} → α, e : l ≃ m, f : o ≃ n. Тогда обновление i-й строки матрицы A на r затем взятие подматрицы по e и f эквивалентно сначала взятию подматрицы A по e и f, а затем обновлению соответствующей строки подматрицы: (A.updateRow i r).submatrix e f = updateRow (A.submatrix e f) (e.symm i) (λ k, r (f k)).
LaTeX
$$$$ (A.updateRow i r).submatrix e f = updateRow \ (A.submatrix e f) (e.symm\, i) (\lambda k,\ r (f\, k)) $$$$
Lean4
theorem submatrix_updateRow_equiv [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : m) (r : n → α) (e : l ≃ m)
(f : o ≃ n) : (A.updateRow i r).submatrix e f = updateRow (A.submatrix e f) (e.symm i) fun i => r (f i) :=
Eq.trans (by simp_rw [Equiv.apply_symm_apply]) (updateRow_submatrix_equiv A _ _ e f).symm
