updateRow_ne

Mathlib.LinearAlgebra.Matrix.RowCol

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

← MathLib Explorer

English

For DecidableEq m, if i' ≠ i then updateRow M i b i' = M i'.

Русский

Для DecidableEq m: если i' ≠ i, то updateRow M i b i' = M i'.

LaTeX

$$$ \text{[DecidableEq m]}\ {i' : m},\ i' \neq i \Rightarrow\ updateRow M i b i' = M i' $$$

Lean4

@[simp]
theorem updateRow_ne [DecidableEq m] {i' : m} (i_ne : i' ≠ i) : updateRow M i b i' = M i' :=
  Function.update_of_ne (β := fun _ => (n → α)) i_ne b M

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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