adjugate_conjTranspose — Mathlib

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]

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