English
There exists a bilinear map that assigns to a pair of matrices A and B the Kronecker product A ⊗_R B, landing in matrices with entries in α ⊗_R β; the map is linear in each argument over the appropriate scalars.
Русский
Существует билинеарное отображение, задающее для пары матриц A и B их кронекерово произведение A ⊗_R B, принадлежащее матрицам с элементами в α ⊗_R β; отображение линейно по каждому аргументу относительно соответствующих скаляров.
LaTeX
$$$\text{kroneckerTMulBilinear} : M_{l,m}(\alpha) \times M_{n,p}(\beta) \to M_{l\times n,\, m\times p}(\alpha \otimes_R \beta)$ is a bilinear map, i.e. linear in each argument over the appropriate scalars.$$
Lean4
/-- `Matrix.kronecker` as a bilinear map. -/
def kroneckerTMulBilinear [Semiring S] [Module S α] [SMulCommClass R S α] :
Matrix l m α →ₗ[S] Matrix n p β →ₗ[R] Matrix (l × n) (m × p) (α ⊗[R] β) :=
kroneckerMapBilinear (AlgebraTensorModule.mk _ _ α β)
