adjugate_fin_two — Mathlib

English

For a 2×2 matrix A, adjugate A equals the standard adjugate matrix [[d, -b], [-c, a]].

Русский

Для 2×2 матрицы A adjugate(A) = [[d, -b], [-c, a]].

LaTeX

$$$\operatorname{adj}\begin{pmatrix}a&b\\ c&d\end{pmatrix} = \begin{pmatrix}d & -b\\ -c & a\end{pmatrix}$$$

Lean4

theorem adjugate_fin_two (A : Matrix (Fin 2) (Fin 2) α) : adjugate A = !![A 1 1, -A 0 1; -A 1 0, A 0 0] :=
  by
  ext i j
  rw [adjugate_fin_succ_eq_det_submatrix]
  fin_cases i <;> fin_cases j <;> simp

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