English
Replacing a column by a linear combination of columns multiplies the determinant by the coefficient of that column.
Русский
Замена столбца на линейную комбинацию столбцов умножает детерминант на коэффициент этого столбца.
LaTeX
$$det( updateCol(A, j, fun k => \\sum i, (c i) • A_{k i}) ) = (c j) • det A$$
Lean4
/-- If we replace a column of a matrix by a linear combination of its columns, then the determinant
is multiplied by the coefficient of that column. -/
theorem det_updateCol_sum (A : Matrix n n R) (j : n) (c : n → R) :
(A.updateCol j (fun k ↦ ∑ i, (c i) • A k i)).det = (c j) • A.det :=
by
rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]
convert det_updateRow_sum A.transpose j c
simp only [smul_eq_mul, Finset.sum_apply, Pi.smul_apply, transpose_apply]
