adjugate_fin_succ_eq_det_submatrix

English

For A of size Fin(n.succ), the (i,j) entry of adjugate is (-1)^{i+j} times the determinant of A with row j and column i removed (the appropriate minor).

Русский

Для матрицы размера Fin(n.succ) i-й ряд и j-й столбец исключаются, и соответствующая мина det даёт элемент adjugate(A)_{i j} = (−1)^{i+j} det(минор).

LaTeX

$$$\operatorname{adj}(A)_{i j} = (-1)^{i+j} \det\bigl(A_{j\text{}i}\bigr)$$$

Lean4

theorem adjugate_fin_succ_eq_det_submatrix {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) α) (i j) :
    adjugate A i j = (-1) ^ (j + i : ℕ) * det (A.submatrix j.succAbove i.succAbove) :=
  by
  simp_rw [adjugate_apply, det_succ_row _ j, updateRow_self, submatrix_updateRow_succAbove]
  rw [Fintype.sum_eq_single i fun h hjk => ?_, Pi.single_eq_same, mul_one]
  rw [Pi.single_eq_of_ne hjk, mul_zero, zero_mul]

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