English
Updating a diagonal matrix by replacing the i-th column 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-я компонента обновлена до x.
LaTeX
$$$$ (\\operatorname{diagonal} v).updateCol i (\\operatorname{Pi}.single i x) = \\operatorname{diagonal}(\\operatorname{Function.update} v i x) $$$$
Lean4
theorem diagonal_updateCol_single [DecidableEq n] [Zero α] (v : n → α) (i : n) (x : α) :
(diagonal v).updateCol i (Pi.single i x) = diagonal (Function.update v i x) :=
by
ext j k
obtain rfl | hjk := eq_or_ne j k
· rw [diagonal_apply_eq]
obtain rfl | hji := eq_or_ne j i
· rw [updateCol_self, Pi.single_eq_same, Function.update_self]
· rw [updateCol_ne hji, diagonal_apply_eq, Function.update_of_ne hji]
· rw [diagonal_apply_ne _ hjk]
obtain rfl | hki := eq_or_ne k i
· rw [updateCol_self, Pi.single_eq_of_ne hjk]
· rw [updateCol_ne hki, diagonal_apply_ne _ hjk]
