transpose_list_prod — Mathlib

English

The transpose of the product of a list of square matrices equals the reverse-ordered product of their transposes.

Русский

Транспонирование произведения списка квадратных матриц эквивалентно произведению транспонированных в обратном порядке.

LaTeX

$$$\mathrm{transpose}(l_{1} \cdot l_{2} \cdot \dots) = (l_{1}^T \cdot l_{2}^T \cdot \dots)^{\text{reverse}}$ for a finite list l of square matrices.$$

Lean4

theorem transpose_list_prod [CommSemiring α] [Fintype m] [DecidableEq m] (l : List (Matrix m m α)) :
    l.prodᵀ = (l.map transpose).reverse.prod :=
  (transposeRingEquiv m α).unop_map_list_prod l

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