conjTranspose_map — Mathlib

English

If f is a semiconjugation between the star operations, then conjugate transpose commutes with applying f to all entries: (A^H).map f = (A.map f)^H.

Русский

Если f является полусопряжением между операциями звезды, то сопряжённое транспонирование коммутирует с применением f к каждому элементу: A^H.map f = (A.map f)^H.

LaTeX

$$$ A^H.map f = (A.map f)^H $$$

Lean4

theorem conjTranspose_map [Star α] [Star β] {A : Matrix m n α} (f : α → β) (hf : Function.Semiconj f star star) :
    Aᴴ.map f = (A.map f)ᴴ :=
  Matrix.ext fun _ _ => hf _

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