English
If a row is replaced by a linear combination of all rows with coefficients c_k, then det becomes c_j times det A.
Русский
Если строка j заменяется линейной комбинацией всех строк с коэффициентами c_k,Det(A) становится c_j Det(A).
LaTeX
$$(A.updateRow j (\\\\sum_k (c_k) A_k)).det = (c_j) \\\\cdot det A$$
Lean4
theorem det_updateRow_sum_aux (M : Matrix n n R) {j : n} (s : Finset n) (hj : j ∉ s) (c : n → R) (a : R) :
(M.updateRow j (a • M j + ∑ k ∈ s, (c k) • M k)).det = a • M.det := by
induction s using Finset.induction_on with
| empty => rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_eq_self]
| insert k _ hk h_ind =>
have h : k ≠ j := fun h ↦ (h ▸ hj) (Finset.mem_insert_self _ _)
rw [Finset.sum_insert hk, add_comm ((c k) • M k), ← add_assoc, det_updateRow_add, det_updateRow_smul,
det_updateRow_eq_zero h, mul_zero, add_zero, h_ind]
exact fun h ↦ hj (Finset.mem_insert_of_mem h)
