det_updateRow_add — Mathlib

English

det replacing a column by a sum equals the sum of determinants with summands.

Русский

Детерминант по столбцу линейен по столбцу: замена столбца на сумму равна сумме детерминантов с каждым слагаемым.

LaTeX

$$det( updateCol(M, j, u + v) ) = det( updateCol(M, j, u) ) + det( updateCol(M, j, v) )$$

Lean4

theorem det_updateRow_add (M : Matrix n n R) (j : n) (u v : n → R) :
    det (updateRow M j <| u + v) = det (updateRow M j u) + det (updateRow M j v) :=
  (detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_update_add M j u v

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