updateRow_eq_self — Mathlib

English

Updating a column twice is idempotent: (A.updateCol j x).updateCol j y = A.updateCol j y, and similarly for updateRow with transposition.

Русский

Обновление столбца дважды идемпотентно: (A.updateCol j x).updateCol j y = A.updateCol j y, аналогично и для обновления строки.

LaTeX

$$$$ (A.updateCol j x).updateCol j y = A.updateCol j y \\text{ and } (A.updateRow i x).updateRow i y = A.updateRow i y $$$$

Lean4

@[simp]
theorem updateRow_eq_self [DecidableEq m] (A : Matrix m n α) (i : m) : A.updateRow i (A i) = A :=
  Function.update_eq_self i A

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