adjugate_fin_two_of

Mathlib.LinearAlgebra.Matrix.Adjugate

URI: https://scilib.ai/kg/mathlib#Matrix.adjugate_fin_two_of

English

For A = [[a,b],[c,d]], adjugate A equals [[d,-b],[-c,a]] (explicit formula).

Русский

Для A = [[a, b], [c, d]] выполняется 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

@[simp]
theorem adjugate_fin_two_of (a b c d : α) : adjugate !![a, b; c, d] = !![d, -b; -c, a] :=
  adjugate_fin_two _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru