updateRow_submatrix_equiv — Mathlib

English

Updating a row in a submatrix corresponds to updating the corresponding row in the original matrix and then taking the submatrix.

Русский

Обновление строки в подматрице эквивалентно обновлению соответствующей строки в исходной матрице и затем взятию подматрицы.

LaTeX

$$$$ \\text{updateRow}(A_{\\text{submatrix}}, i, r) = (A.updateRow( e i )\\, (\\lambda j, r (f^{-1}(j))))_{\\text{submatrix}} $$$$

Lean4

theorem updateRow_submatrix_equiv [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α) (e : l ≃ m)
    (f : o ≃ n) : updateRow (A.submatrix e f) i r = (A.updateRow (e i) fun j => r (f.symm j)).submatrix e f :=
  by
  ext i' j
  simp only [submatrix_apply, updateRow_apply, Equiv.apply_eq_iff_eq, Equiv.symm_apply_apply]

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