det_updateCol_add_smul_self — Mathlib

English

If i ≠ j, det(updateCol A i (A_i + c A_j)) = det A.

Русский

Если i ≠ j, det(updateCol A i (A_i + c A_j)) = det A.

LaTeX

$$i \\\\neq j \\\\Rightarrow \\\\det(\\\\text{updateCol}(A, i, A_i + c \\\\cdot A_j)) = \\\\det A$$

Lean4

theorem det_updateCol_add_smul_self (A : Matrix n n R) {i j : n} (hij : i ≠ j) (c : R) :
    det (updateCol A i fun k => A k i + c • A k j) = det A :=
  by
  rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]
  exact det_updateRow_add_smul_self Aᵀ hij c

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