updateRow_idem — Mathlib

English

Updating a row with two successive vectors x and y is equivalent to updating with y: (A.updateRow i x).updateRow i y = A.updateRow i y.

Русский

Обновление строки двумя векторами x и y эквивалентно обновлению только y: (A.updateRow i x).updateRow i y = A.updateRow i y.

LaTeX

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

Lean4

@[simp]
theorem updateRow_idem [DecidableEq m] (A : Matrix m n α) (i : m) (x y : n → α) :
    (A.updateRow i x).updateRow i y = A.updateRow i y :=
  Function.update_idem _ _ _

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