English
A determinant remains the same under a row-wise addition pattern described in the auxiliary form, valid for matrices of size n+1.
Русский
Детерминант сохраняется при добавлении строк в соответствии с дополнительной формулой для матриц размера n+1.
LaTeX
$$$\\det M = \\det N$ \\\\text{under the auxiliary row-addition pattern with a fixed index } k$$
Lean4
theorem det_eq_of_forall_row_eq_smul_add_pred_aux {n : ℕ} (k : Fin (n + 1)) :
∀ (c : Fin n → R) (_hc : ∀ i : Fin n, k < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
(_h0 : ∀ j, M 0 j = N 0 j) (_hsucc : ∀ (i : Fin n) (j), M i.succ j = N i.succ j + c i * M (Fin.castSucc i) j),
det M = det N :=
by
refine Fin.induction ?_ (fun k ih => ?_) k <;> intro c hc M N h0 hsucc
· congr
ext i j
refine Fin.cases (h0 j) (fun i => ?_) i
rw [hsucc, hc i (Fin.succ_pos _), zero_mul, add_zero]
set M' := updateRow M k.succ (N k.succ) with hM'
have hM : M = updateRow M' k.succ (M' k.succ + c k • M (Fin.castSucc k)) :=
by
ext i j
by_cases hi : i = k.succ
· simp [hi, hM', hsucc, updateRow_self]
rw [updateRow_ne hi, hM', updateRow_ne hi]
have k_ne_succ : (Fin.castSucc k) ≠ k.succ := (Fin.castSucc_lt_succ k).ne
have M_k : M (Fin.castSucc k) = M' (Fin.castSucc k) := (updateRow_ne k_ne_succ).symm
rw [hM, M_k, det_updateRow_add_smul_self M' k_ne_succ.symm, ih (Function.update c k 0)]
· intro i hi
rw [Fin.lt_iff_val_lt_val, Fin.coe_castSucc, Fin.val_succ, Nat.lt_succ_iff] at hi
rw [Function.update_apply]
split_ifs with hik
· rfl
exact hc _ (Fin.succ_lt_succ_iff.mpr (lt_of_le_of_ne hi (Ne.symm hik)))
· rwa [hM', updateRow_ne (Fin.succ_ne_zero _).symm]
intro i j
rw [Function.update_apply]
split_ifs with hik
· rw [zero_mul, add_zero, hM', hik, updateRow_self]
rw [hM', updateRow_ne ((Fin.succ_injective _).ne hik), hsucc]
by_cases hik2 : k < i
· simp [hc i (Fin.succ_lt_succ_iff.mpr hik2)]
rw [updateRow_ne]
apply ne_of_lt
rwa [Fin.lt_iff_val_lt_val, Fin.coe_castSucc, Fin.val_succ, Nat.lt_succ_iff, ← not_lt]
