English
If A is a matrix over a star ring, adjugate commutes with conjugation: adj(A) = adj(A) under star, and adj(A) transforms accordingly.
Русский
Если матрица A над звездным кольцом, adj(A) сохраняется при звездовом преобразовании и ведет себя соответствующим образом.
LaTeX
$$$\operatorname{adj}(A^{*}) = (\operatorname{adj}(A))^{*}$$$
Lean4
theorem adjugate_conjTranspose [StarRing α] (A : Matrix n n α) : A.adjugateᴴ = adjugate Aᴴ :=
by
dsimp only [conjTranspose]
have : Aᵀ.adjugate.map star = adjugate (Aᵀ.map star) := (starRingEnd α).map_adjugate Aᵀ
rw [A.adjugate_transpose, this]