updateRow_comm — Mathlib

English

If i ≠ i', then updating row i then i' equals updating i' then i: (A.updateRow i x).updateRow i' y = (A.updateRow i' y).updateRow i x.

Русский

Если i ≠ i', обновление строк происходит в любом порядке: (A.updateRow i x).updateRow i' y = (A.updateRow i' y).updateRow i x.

LaTeX

$$$$ (A.updateRow i x).updateRow i' y = (A.updateRow i' y).updateRow i x $$$$

Lean4

theorem updateRow_comm [DecidableEq m] (A : Matrix m n α) {i i' : m} (h : i ≠ i') (x y : n → α) :
    (A.updateRow i x).updateRow i' y = (A.updateRow i' y).updateRow i x :=
  Function.update_comm h _ _ _

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