det_updateCol_smul — Mathlib

English

det(updateRow (s • M) j u) = s^(|n| - 1) · det(updateRow M j u).

Русский

Детерминант при умножении всей матрицы на скаляр и последующем изменении одной строки: det(updateRow (s • M) j u) = s^{|n|-1} det(updateRow M j u).

LaTeX

$$det(updateRow(M, j, s \\cdot u)) = s^{( |n| - 1 )} \\\\cdot det(updateRow(M, j, u))$$

Lean4

theorem det_updateCol_smul (M : Matrix n n R) (j : n) (s : R) (u : n → R) :
    det (updateCol M j <| s • u) = s * det (updateCol M j u) :=
  by
  rw [← det_transpose, ← updateRow_transpose, det_updateRow_smul]
  simp [updateRow_transpose, det_transpose]

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