updateCol_idem — Mathlib

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

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