English
The adjugate of A is the matrix whose i-th row is given by the cramer map on Aᵀ with the i-th unit column.
Русский
Смежная матрица adjugate A задаётся как транспонированная матрица кофакторов, реализуемая через карту cramer.
LaTeX
$$$$\\operatorname{adjugate}(A) = \\mathrm{of}\\; i \\mapsto \\mathrm{cramer}(A^{\\top}, \\mathbf{e}_i).$$$$
Lean4
/-- The adjugate matrix is the transpose of the cofactor matrix.
Typically, the cofactor matrix is defined by taking minors,
i.e. the determinant of the matrix with a row and column removed.
However, the proof of `mul_adjugate` becomes a lot easier if we use the
matrix replacing a column with a basis vector, since it allows us to use
facts about the `cramer` map.
-/
def adjugate (A : Matrix n n α) : Matrix n n α :=
of fun i => cramer Aᵀ (Pi.single i 1)
