English
Adding multiples of one row to another row does not change the determinant.
Русский
Прибавление к одной строке кратных другой строки не меняет детерминант.
LaTeX
$$$\\det A = \\det B$ \\\\text{whenever } A_{ij} = B_{ij} + c_i B_{k j} \\text{ for all } i,j \\text{ with } c_k = 0$$
Lean4
theorem det_eq_of_forall_row_eq_smul_add_const_aux {A B : Matrix n n R} {s : Finset n} :
∀ (c : n → R) (_ : ∀ i, i ∉ s → c i = 0) (k : n) (_ : k ∉ s) (_ : ∀ i j, A i j = B i j + c i * B k j),
det A = det B :=
by
induction s using Finset.induction_on generalizing B with
| empty =>
rintro c hs k - A_eq
have : ∀ i, c i = 0 := by grind
congr
ext i j
rw [A_eq, this, zero_mul, add_zero]
| insert i s _hi ih =>
intro c hs k hk A_eq
have hAi : A i = B i + c i • B k := funext (A_eq i)
rw [@ih (updateRow B i (A i)) (Function.update c i 0), hAi, det_updateRow_add_smul_self]
· exact mt (fun h => show k ∈ insert i s from h ▸ Finset.mem_insert_self _ _) hk
· intro i' hi'
rw [Function.update_apply]
split_ifs with hi'i
· rfl
· exact hs i' fun h => hi' ((Finset.mem_insert.mp h).resolve_left hi'i)
· exact k
· exact fun h => hk (Finset.mem_insert_of_mem h)
· intro i' j'
rw [updateRow_apply, Function.update_apply]
split_ifs with hi'i
· simp [hi'i]
rw [A_eq, updateRow_ne fun h : k = i => hk <| h ▸ Finset.mem_insert_self k s]
