English
There is a linear equivalence between block-mstructured matrices and matrices with product-indexed rows and columns, compatible with scalar multiplication.
Русский
Существует линейное эквивалентное отображение между матрицами блочной структуры и матрицами с индексами строк и столбцов, заданное через compAddEquiv, совместимое с умножением на скаляры.
LaTeX
$$$ \mathrm{compLinearEquiv} : \mathrm{Matrix} I J (\mathrm{Matrix} K L R) \simeq_{K} \mathrm{Matrix} (I \times K) (J \times L) R $$$
Lean4
/-- `Matrix.comp` as `LinearEquiv` -/
@[simps!]
def compLinearEquiv : Matrix I J (Matrix K L R) ≃ₗ[K] Matrix (I × K) (J × L) R
where
__ := Matrix.compAddEquiv I J K L R
map_smul' _ _ := rfl
