English
Similarly, det(A) = sum_i A_{i j} adj(A)_{j i} for any fixed column j.
Русский
Аналогично, детерминант равен сумме по i: det(A) = ∑_i A_{i j} adj(A)_{j i} для фиксированного столбца j.
LaTeX
$$$\det(A) = \sum_{i} A_{i j} \operatorname{adj}(A)_{j i}$$$
Lean4
theorem det_eq_sum_mul_adjugate_row (A : Matrix n n α) (i : n) : det A = ∑ j : n, A i j * adjugate A j i :=
by
haveI : Nonempty n := ⟨i⟩
obtain ⟨n', hn'⟩ := Nat.exists_eq_succ_of_ne_zero (Fintype.card_ne_zero : Fintype.card n ≠ 0)
obtain ⟨e⟩ := Fintype.truncEquivFinOfCardEq hn'
let A' := reindex e e A
suffices det A' = ∑ j : Fin n'.succ, A' (e i) j * adjugate A' j (e i)
by
simp_rw [A', det_reindex_self, adjugate_reindex, reindex_apply, submatrix_apply, ← e.sum_comp,
Equiv.symm_apply_apply] at this
exact this
rw [det_succ_row A' (e i)]
simp_rw [mul_assoc, mul_left_comm _ (A' _ _), ← adjugate_fin_succ_eq_det_submatrix]
