updateCol_conjTranspose — Mathlib

English

Updating different rows (or columns) in a matrix commutes when the indices are distinct: updating row i then row i' equals updating row i' then row i.

Русский

Обновление разных строк в матрице коммутирует, если индексы различны: обновление строки i затем i' равно обновлению i' затем i.

LaTeX

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

Lean4

theorem updateCol_conjTranspose [DecidableEq m] [Star α] : updateCol Mᴴ i (star b) = (updateRow M i b)ᴴ :=
  by
  rw [conjTranspose, conjTranspose, transpose_map, transpose_map, updateCol_transpose, map_updateRow]
  rfl

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