updateCol_self

Mathlib.LinearAlgebra.Matrix.RowCol

URI: https://scilib.ai/kg/mathlib#Matrix.updateCol_self

English

For DecidableEq m, updateCol M^T i b = (updateRow M i b)ᵀ.

Русский

Для DecidableEq m верно: updateCol M^T i b = (updateRow M i b)ᵀ.

LaTeX

$$$ \mathrm{updateCol}\ M^T\ i\ b = (\mathrm{updateRow}\ M\ i\ b)^T $$$

Lean4

@[simp]
theorem updateCol_self [DecidableEq n] : updateCol M j c i j = c i :=
  Function.update_self (β := fun _ => α) j (c i) (M i)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru