map_adjugate — Mathlib

English

In the generalized setting, an AlgHom preserves adjugate: f.mapMatrix(A.adjugate) = Matrix.adjugate(f.mapMatrix A).

Русский

В обобщённом случае AlgHom сохраняет adjugate: f.mapMatrix(A.adjugate) = adjugate(f.mapMatrix A).

LaTeX

$$$f.mapMatrix(A.adjugate) = \operatorname{adjugate}(f.mapMatrix(A))$$$

Lean4

theorem _root_.AlgHom.map_adjugate {R A B : Type*} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A]
    [Algebra R B] (f : A →ₐ[R] B) (M : Matrix n n A) : f.mapMatrix M.adjugate = Matrix.adjugate (f.mapMatrix M) :=
  f.toRingHom.map_adjugate _

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