English
Kronecker product is defined as a bilinear map: the map kroneckerMapBilinear takes a bilinear map f and returns a bilinear map on matrices by Kronecker-structuring the inputs.
Русский
Кронекерово произведение задаётся как билинейное отображение: kroneckerMapBilinear принимает билинейное отображение f и возвращает билинейное отображение на матрицах через операцию Кронекера.
LaTeX
$$$\operatorname{kroneckerMapBilinear} : (\alpha \to\beta \to\gamma) \to\mathrm{Matrix}\ l m\alpha \to\mathrm{Matrix}\ n p\beta \to\mathrm{Matrix} (l \times n) (m \times p) \gamma$$$
Lean4
/-- When `f` is bilinear then `Matrix.kroneckerMap f` is also bilinear. -/
@[simps!]
def kroneckerMapBilinear [Semiring S] [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α]
[Module R γ] [Module S β] [Module S γ] [SMulCommClass S R γ] (f : α →ₗ[R] β →ₗ[S] γ) :
Matrix l m α →ₗ[R] Matrix n p β →ₗ[S] Matrix (l × n) (m × p) γ :=
LinearMap.mk₂' R S (kroneckerMap fun r s => f r s) (kroneckerMap_add_left _ <| f.map_add₂)
(fun _ => kroneckerMap_smul_left _ _ <| f.map_smul₂ _) (kroneckerMap_add_right _ fun a => (f a).map_add) fun r =>
kroneckerMap_smul_right _ _ fun a => (f a).map_smul r
