det_neg_eq_smul — Mathlib

English

Multiplying each row i by a fixed v_i scales the determinant by the product of all v_i: det((i,j) ↦ v_i A_{ij}) = (∏ i v_i) det A.

Русский

Умножение i-й строки на фиксированное v_i масштабирует детерминант на произведение всех v_i: det((i,j) ↦ v_i A_{ij}) = (∏ i v_i) det A.

LaTeX

$$$$\det\left((i,j) \mapsto v_i A_{ij}\right) = \left(\prod_i v_i\right) \det A,$$ где $v_i$ задана на индексе строк.$$

Lean4

/-- A variant of `Matrix.det_neg` with scalar multiplication by `Units ℤ` instead of multiplication
by `R`. -/
theorem det_neg_eq_smul (A : Matrix n n R) : det (-A) = (-1 : Units ℤ) ^ Fintype.card n • det A := by
  rw [← det_smul_of_tower, Units.neg_smul, one_smul]

Похожие утверждения