English
The linear map built from TensorProduct.map f g corresponds to the Kronecker product of the matrices of f and g.
Русский
Линейное отображение, полученное из TensorProduct.map f g, соответствует Kronecker произведению матриц f и g.
LaTeX
$$$toLin (bM \otimes bN) (bM' \otimes bN') (A \otimes_κ B) = \mathrm{toLin}\ bM bM' A \otimes_κ \mathrm{toLin} bN bN' B$$$
Lean4
/-- The matrix built from `Matrix.kronecker` corresponds to the linear map built from
`TensorProduct.map`. -/
theorem toLin_kronecker (A : Matrix ι' ι R) (B : Matrix κ' κ R) :
toLin (bM.tensorProduct bN) (bM'.tensorProduct bN') (A ⊗ₖ B) =
TensorProduct.map (toLin bM bM' A) (toLin bN bN' B) :=
by rw [← LinearEquiv.eq_symm_apply, toLin_symm, TensorProduct.toMatrix_map, toMatrix_toLin, toMatrix_toLin]
