English
Let I, J, K, L, R, R' be types with I and J finite, K a commutative semiring, R a semiring, an algebra structure of R over K, and decidable equality on I and J. Then the canonical algebra isomorphism compAlgEquiv I J R K acts identically (on M) to the direct composition map comp I I J J R, i.e., compAlgEquiv I J R K M = comp I I J J R M for all M : Matrix I I (Matrix J J R).
Русский
Пусть I, J, K, L, R, R' — множества, I и J — конечны, K — коммутативная полугруппа, R — полугруппа, имеется структура алгебры над K, и задано равенство по элементам на I и J. Тогда каноническое алгебраическое изоморфизм compAlgEquiv I J R K действует на M так же, как прямая композиционная карта comp I I J J R, т.е. для всякой M: Matrix I I (Matrix J J R) выполняется compAlgEquiv I J R K M = comp I I J J R M.
LaTeX
$$$\\operatorname{compAlgEquiv}_{I,J,R,K}(M) = \\operatorname{comp}_{I,I,J,J,R}(M)$$$
Lean4
@[simp]
theorem compAlgEquiv_apply (M : Matrix I I (Matrix J J R)) : compAlgEquiv I J R K M = comp I I J J R M :=
rfl
