conjTranspose_list_prod — Mathlib

English

For a list l of square matrices, the conjugate transpose of the list product equals the reverse product of their conjugate transposes.

Русский

Для списка квадратных матриц l сопряжённое транспонирование произведения списка равно обратному порядку произведения сопряжённых транспонированных матриц.

LaTeX

$$$ \text{conjTransposeListProd}[l] : (\text{prod}_{M \in l} M)^H = \prod^{\leftarrow}_{M \in l} M^H $$$

Lean4

theorem conjTranspose_list_prod [Semiring α] [StarRing α] [Fintype m] [DecidableEq m] (l : List (Matrix m m α)) :
    l.prodᴴ = (l.map conjTranspose).reverse.prod :=
  (conjTransposeRingEquiv m α).unop_map_list_prod l

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