English
For j, a finite set s disjoint from {j}, and coefficients c, a, det of updating row j by a·M_j + sum_{k∈s} c_k M_k equals a times det M.
Русский
Для фиксированной строки j и множества s, не содержащего j, и коэффициентов c_k, a: det обновления строки j до a·M_j + ∑_{k∈s} c_k M_k равно a·det M.
LaTeX
$$det( updateRow(M, j, a \\cdot M_j + ∑_{k ∈ s} (c_k) \\cdot M_k) ) = a \\\\cdot det(M)$$
Lean4
theorem det_updateCol_smul_left (M : Matrix n n R) (j : n) (s : R) (u : n → R) :
det (updateCol (s • M) j u) = s ^ (Fintype.card n - 1) * det (updateCol M j u) :=
by
rw [← det_transpose, ← updateRow_transpose, transpose_smul, det_updateRow_smul_left]
simp [updateRow_transpose, det_transpose]