diagonal_updateRow_single — Mathlib

English

Updating a diagonal matrix by replacing the i-th row with the i-th unit vector scaled by x yields the diagonal matrix with the i-th entry updated to x.

Русский

Обновление диагонали по строке: замена i-й строки на Pi.single i x дает диагональ с обновлённой i-й компонентой.

LaTeX

$$$$ (\\operatorname{diagonal} v).updateRow i (\\operatorname{Pi}.single i x) = \\operatorname{diagonal}(\\operatorname{Function.update} v i x) $$$$

Lean4

theorem diagonal_updateRow_single [DecidableEq n] [Zero α] (v : n → α) (i : n) (x : α) :
    (diagonal v).updateRow i (Pi.single i x) = diagonal (Function.update v i x) := by
  rw [← diagonal_transpose, updateRow_transpose, diagonal_updateCol_single, diagonal_transpose]

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