adjugate_fin_three_of — Mathlib

English

For any A and row index i, det(A) = sum_j A_{i j} adj(A)_{j i}.

Русский

Для любой матрицы A и строки i детерминант равен сумме по j: det(A) = ∑_j A_{i j} adj(A)_{j i}.

LaTeX

$$$\det(A) = \sum_{j} A_{i j} \operatorname{adj}(A)_{j i}$$$

Lean4

@[simp]
theorem adjugate_fin_three_of (a b c d e f g h i : α) :
    adjugate !![a, b, c; d, e, f; g, h, i] =
      !![e * i - f * h, -(b * i) + c * h, b * f - c * e;
        -(d * i) + f * g, a * i - c * g, -(a * f) + c * d;
        d * h - e * g, -(a * h) + b * g, a * e - b * d] :=
  adjugate_fin_three _

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