English
Multiplying each column i by a fixed v_i scales the determinant by the product of all v_i: det((i,j) ↦ v_j A_{ij}) = (∏ j v_j) det A.
Русский
Умножение i-го столбца на фиксированное v_i масштабирует детерминант на произведение всех v_i: det((i,j) ↦ v_j A_{ij}) = (∏ j v_j) det A.
LaTeX
$$$$\det\left((i,j) \mapsto v_j A_{ij}\right) = \left(\prod_j v_j\right) \det A,$$ где $v_j$ — задание на индексе столбцов.$$
Lean4
/-- Multiplying each row by a fixed `v i` multiplies the determinant by
the product of the `v`s. -/
theorem det_mul_row (v : n → R) (A : Matrix n n R) : det (of fun i j => v j * A i j) = (∏ i, v i) * det A :=
calc
det (of fun i j => v j * A i j) = det (A * diagonal v) :=
congr_arg det <| by
ext
simp [mul_comm]
_ = (∏ i, v i) * det A := by rw [det_mul, det_diagonal, mul_comm]
