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