det_updateCol_add — Mathlib

English

det of updating a row by s times a vector equals s times det after update.

Русский

Детерминант при умножении одной строки на скаляр сохраняется линейной зависимостью: det(updateRow M j (s • u)) = s · det(updateRow M j u).

LaTeX

$$det(updateRow(M, j, s \\cdot u)) = s \\cdot det(updateRow(M, j, u))$$

Lean4

theorem det_updateCol_add (M : Matrix n n R) (j : n) (u v : n → R) :
    det (updateCol M j <| u + v) = det (updateCol M j u) + det (updateCol M j v) :=
  by
  rw [← det_transpose, ← updateRow_transpose, det_updateRow_add]
  simp [updateRow_transpose, det_transpose]

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