English
Updating a column twice is idempotent: (A.updateCol j x).updateCol j y = A.updateCol j y.
Русский
Обновление столбца дважды идемпотентно: (A.updateCol j x).updateCol j y = A.updateCol j y.
LaTeX
$$$$ (A.updateCol j x).updateCol j y = A.updateCol j y $$$$
Lean4
@[simp]
theorem updateCol_idem [DecidableEq n] (A : Matrix m n α) (j : n) (x y : m → α) :
(A.updateCol j x).updateCol j y = A.updateCol j y := by
simpa only [updateRow_transpose] using congr_arg transpose <| updateRow_idem Aᵀ j x y