English
There is a canonical linear map that sends a matrix Y to the linear operator X ↦ X · Y, i.e., right multiplication by Y, which is linear in Y and respects addition and scalar multiplication.
Русский
Существуют канонические линейные отображения, отправляющие матрицу Y в линейный оператор X ↦ X · Y, то есть правое умножение на Y, линейно по Y и сохраняющее сумму и умножение на скаляр.
LaTeX
$$$$\\mathrm{mulRightLinearMap} \\colon \\mathrm{Mat}(m,n,A) \\to_{\\\\mathbb{R}} \\mathrm{Mat}(l,n,A) \\to_{\\\\mathbb{R}} \\mathrm{Mat}(l,n,A)\\; (Y) = (X \\mapsto X Y).$$$$
Lean4
/-- A version of `LinearMap.mulRight` for matrix multiplication. -/
@[simps]
def mulRightLinearMap (Y : Matrix m n A) : Matrix l m A →ₗ[R] Matrix l n A
where
toFun := (· * Y)
map_smul' _ _ := Matrix.smul_mul _ _ _
map_add' _ _ := Matrix.add_mul _ _ _
