det_updateRow_smul — Mathlib

English

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

Русский

Детерминант по столбцу линейно по столбцу: det(updateCol M j (s • u)) = s · det(updateCol M j u).

LaTeX

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

Lean4

theorem det_updateRow_smul (M : Matrix n n R) (j : n) (s : R) (u : n → R) :
    det (updateRow M j <| s • u) = s * det (updateRow M j u) :=
  (detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_update_smul M j s u

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