comp_map_transpose — Mathlib

English

Applying transpose to all entries commutes with the matrix comp operation: comp I J L K R (M^T) = (comp I J K L R M^T)^T.

Русский

Применение транспонирования ко всем элементам коммутирует с операцией comp: comp I J L K R (M^T) = (comp I J K L R M^T)^T.

LaTeX

$$$ \mathrm{comp}_{I J L K R}(M^{T}) = \bigl(\mathrm{comp}_{I J K L R}(M^{T})\bigr)^{T} $$$

Lean4

theorem comp_map_transpose (M : Matrix I J (Matrix K L R)) : comp I J L K R (M.map (·ᵀ)) = (comp _ _ _ _ R Mᵀ)ᵀ :=
  rfl

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