English
A determinant is unchanged under a controlled row addition pattern: if A and B satisfy A_ij = B_ij + c_i B_kj with c_k = 0 and the specified relations, then det A = det B.
Русский
Детерминант не меняется при определённом порядке добавления кратных одной строки к другим строкам: если матрицы A и B удовлетворяют A_ij = B_ij + c_i B_kj с c_k = 0 и другими условиями, то det A = det B.
LaTeX
$$$\\det A = \\det B$ \\\\text{whenever } A_{ij} = B_{ij} + c_i B_{k j}, \\; c_k = 0 \\\\text{for all } i,j$$
Lean4
/-- If you add multiples of row `B k` to other rows, the determinant doesn't change. -/
theorem det_eq_of_forall_row_eq_smul_add_const {A B : Matrix n n R} (c : n → R) (k : n) (hk : c k = 0)
(A_eq : ∀ i j, A i j = B i j + c i * B k j) : det A = det B :=
det_eq_of_forall_row_eq_smul_add_const_aux c
(fun i =>
not_imp_comm.mp fun hi =>
Finset.mem_erase.mpr ⟨mt (fun h : i = k => show c i = 0 from h.symm ▸ hk) hi, Finset.mem_univ i⟩)
k (Finset.notMem_erase k Finset.univ) A_eq
