English
The Kronecker TMul linear equivalence respects multiplication; it is compatible with the scalar actions and the tensor product.
Русский
Кронекерово линейное эквивалентное отображение сохраняет умножение; совместимо с действиями скаляров и тензорным произведением.
LaTeX
$$$ kroneckerTMulLinearEquiv(xy) = kroneckerTMulLinearEquiv(x) kroneckerTMulLinearEquiv(y) $$$
Lean4
/-- Note this can't be stated for rectangular matrices because there is no
`HMul (TensorProduct R _ _) (TensorProduct R _ _) (TensorProduct R _ _)` instance. -/
@[simp]
theorem kroneckerTMulLinearEquiv_mul [Module S A] [IsScalarTower R S A] :
∀ x y : Matrix m m A ⊗[R] Matrix n n B,
kroneckerTMulLinearEquiv m m n n R S A B (x * y) =
kroneckerTMulLinearEquiv m m n n R S A B x * kroneckerTMulLinearEquiv m m n n R S A B y :=
(kroneckerTMulLinearEquiv m m n n R S A B).toLinearMap.restrictScalars R |>.map_mul_iff.2 <|
by
ext : 10
simp [single_kroneckerTMul_single, mul_kroneckerTMul_mul]
