adjugate_apply — Mathlib

English

For all i,j, adjugate A i j equals det of A with j-th row replaced by unit vector e_i.

Русский

Для всех i,j: adjugate A_i j = det(A с заменой j-й строки на e_i).

LaTeX

$$$$\\operatorname{adjugate}(A)_{ij} = \\det\\left(A\\text{ with row } j\\text{ replaced by } \\mathbf{e}_i\\right).$$$$

Lean4

theorem adjugate_apply (A : Matrix n n α) (i j : n) : adjugate A i j = (A.updateRow j (Pi.single i 1)).det := by
  rw [adjugate_def, of_apply, cramer_apply, updateCol_transpose, det_transpose]

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