English
Updating a row and then taking the submatrix above the updated index is the same as directly taking the submatrix above the index.
Русский
Обновление строки и последующее взятие подматрицы над обновлённой позицией равно взятию подматрицы над соответствующей позицией без обновления.
LaTeX
$$$\big(A.updateRow(i,v)\big).submatrix(i.succAbove,f) = A.submatrix(i.succAbove,f)$$$
Lean4
/-- Updating a row then removing it is the same as removing it. -/
@[simp]
theorem submatrix_updateRow_succAbove (A : Matrix (Fin m.succ) n' α) (v : n' → α) (f : o' → n') (i : Fin m.succ) :
(A.updateRow i v).submatrix i.succAbove f = A.submatrix i.succAbove f :=
ext fun r s => (congr_fun (updateRow_ne (Fin.succAbove_ne i r) : _ = A _) (f s) :)