comp_symm_transpose — Mathlib

English

Transposing and taking inverses commute with block transpose operations: (comp J I L K R).symm M^T = (((comp I J K L R).symm M).map (·^T))^T.

Русский

Транспонирование и взятие обратной перестановкой сохраняют блочные транспонирования: (comp J I L K R).symm M^T = (((comp I J K L R).symm M).map (·^T))^T.

LaTeX

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

Lean4

theorem comp_symm_transpose (M : Matrix (I × K) (J × L) R) :
    (comp J I L K R).symm Mᵀ = (((comp I J K L R).symm M).map (·ᵀ))ᵀ :=
  rfl

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