English
For any fixed j and s not containing j, and coefficients c, a, det of updated row equals a times det A.
Русский
Для фиксированной строки j и множества s, не содержащего j, det(обновление строки j линейной комбинацией) = a · det A.
LaTeX
$$(M.updateRow j (instHAdd.hAdd (instHSMul.hSMul a (M j)) (s.sum fun k => instHSMul.hSMul (c k) (M k)))).det = a · M.det$$
Lean4
/-- If we replace a row of a matrix by a linear combination of its rows, then the determinant is
multiplied by the coefficient of that row. -/
theorem det_updateRow_sum (A : Matrix n n R) (j : n) (c : n → R) :
(A.updateRow j (∑ k, (c k) • A k)).det = (c j) • A.det :=
by
convert det_updateRow_sum_aux A (Finset.univ.erase j) (Finset.univ.notMem_erase j) c (c j)
rw [← Finset.univ.add_sum_erase _ (Finset.mem_univ j)]
