English
For a 3×3 matrix A, adjugate A is the explicit 3×3 matrix whose entries are the cofactors of A (given by the standard 3×3 adjugate).
Русский
Для 3×3 матрицы A adjugate(A) — это явная 3×3 матрица со сводными cofactors A.
LaTeX
$$\operatorname{adj}(A) = \begin{pmatrix} \Delta_{11} & \Delta_{12} & \Delta_{13} \\ \Delta_{21} & \Delta_{22} & \Delta_{23} \\ \Delta_{31} & \Delta_{32} & \Delta_{33} \end{pmatrix}, \text{ где cofactors } \Delta_{ij} \text{ задаются по правилу cofactors}$$
Lean4
theorem adjugate_fin_three (A : Matrix (Fin 3) (Fin 3) α) :
adjugate A =
!![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
-(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0] :=
by
ext i j
rw [adjugate_fin_succ_eq_det_submatrix, det_fin_two]
fin_cases i <;> fin_cases j <;> simp [Fin.succAbove, Fin.lt_def] <;> ring
