English
There is a ring-equivalence between block-structured matrices and matrices of blocks, given by compAddEquiv together with ring operations.
Русский
Существует кольцевое эквивалентное отображение между матрицами блочной структуры и матрицами блоков, задаваемое через compAddEquiv совместно с кольцевыми операциями.
LaTeX
$$$ \mathrm{compRingEquiv} : \mathrm{Matrix} I I (\mathrm{Matrix} J J R) \simeq_+* \mathrm{Matrix} (I \times J) (I \times J) R $$$
Lean4
/-- `Matrix.comp` as `RingEquiv` -/
def compRingEquiv : Matrix I I (Matrix J J R) ≃+* Matrix (I × J) (I × J) R
where
__ := Matrix.compAddEquiv I I J J R
map_mul' _ _ := by ext; exact (Matrix.sum_apply ..).trans <| .symm <| Fintype.sum_prod_type ..
