English
Let A be a matrix, j : o, c : l → α, e : l ≃ m, f : o ≃ n. Then updating the submatrix by a column at j and then taking the submatrix equals updating the corresponding column of A and then taking the submatrix: updateCol (A.submatrix e f) j c = (A.updateCol (f j) (λ i, c (e.symm i))).submatrix e f.
Русский
Пусть A — матрица, j : o, c : l → α, e : l ≃ m, f : o ≃ n. Тогда обновление подматрицы по столбцу в позиции j и последующее взятие подматрицы эквивалентно обновлению соответствующего столбца матрицы A затем взятию подматрицы: updateCol (A.submatrix e f) j c = (A.updateCol (f j) (λ i, c (e.symm i))).submatrix e f.
LaTeX
$$$$ updateCol (A.submatrix e f) j c = (A.updateCol (f\, j) (\lambda i, c (e.symm\, i))).submatrix e f $$$$
Lean4
theorem updateCol_submatrix_equiv [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : o) (c : l → α) (e : l ≃ m)
(f : o ≃ n) : updateCol (A.submatrix e f) j c = (A.updateCol (f j) fun i => c (e.symm i)).submatrix e f := by
simpa only [← transpose_submatrix, updateRow_transpose] using
congr_arg transpose (updateRow_submatrix_equiv Aᵀ j c f e)
