conjTranspose_reindex — Mathlib

English

If e_m and e_n are equivalences, then reindexing commutes with taking adjoint: (reindex e_m e_n M)^* = reindex e_n e_m M^*.

Русский

Если e_m и e_n — биекция, то перестановка индексов через reindex commuting с сопряжённым: (reindex e_m e_n M)^* = reindex e_n e_m M^*.

LaTeX

$$$(reindex\\ e_m\\ e_n\\ M)^{*} = reindex\\ e_n\\ e_m\\ M^{*}$$$

Lean4

theorem conjTranspose_reindex [Star α] (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) :
    (reindex eₘ eₙ M)ᴴ = reindex eₙ eₘ Mᴴ :=
  rfl

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