det_eq_of_forall_col_eq_smul_add_pred

English

Determinant is unchanged when adding multiples of a column to other columns (pred form).

Русский

Детерминант не изменяется при добавлении кратных столбцов к другим столбцам (pred-форма).

LaTeX

$$$\\det A = \\det B$ \\\\text{when } A_{ij} = B_{ij} + c_j B_{i\,k} \\\\text{for all } i,j$$

Lean4

/-- If you add multiples of previous columns to the next columns, the determinant doesn't change. -/
theorem det_eq_of_forall_col_eq_smul_add_pred {n : ℕ} {A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R} (c : Fin n → R)
    (A_zero : ∀ i, A i 0 = B i 0) (A_succ : ∀ (i) (j : Fin n), A i j.succ = B i j.succ + c j * A i (Fin.castSucc j)) :
    det A = det B := by
  rw [← det_transpose A, ← det_transpose B]
  exact det_eq_of_forall_row_eq_smul_add_pred c A_zero fun i j => A_succ j i

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