submatrix_updateRow_succAbove — Mathlib

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) :)

Похожие утверждения