adjugate_reindex — Mathlib

English

The adjugate commutes with reindexing: adjugate(reindex e e A) = reindex e e (adjugate A).

Русский

Adjugate коммутирует с перестановкой индексов: adjugate(reindex e e A) = reindex e e (adjugate A).

LaTeX

$$$$\\operatorname{adjugate}(\\mathrm{reindex}\\; e\\; e\\; A) = \\mathrm{reindex}\\; e\\; e\\; (\\operatorname{adjugate} A).$$$$

Lean4

theorem adjugate_reindex (e : m ≃ n) (A : Matrix m m α) : adjugate (reindex e e A) = reindex e e (adjugate A) :=
  adjugate_submatrix_equiv_self _ _

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