English
There is a canonical linear map that sends a matrix X to the linear operator Y ↦ X · Y, i.e., left multiplication by X, which is linear in X and respects addition and scalar multiplication.
Русский
Существует каноническое линейное отображение, переводящее матрицу X в линейный оператор Y ↦ X · Y, то есть левое умножение на X, линейно по X и сохраняющее сложение и умножение на скаляр.
LaTeX
$$$$\\mathrm{mulLeftLinearMap} \\\\colon \\, \\mathrm{Mat}(l,m,A) \\\\to_{\\\\mathbb{R}} \\mathrm{Mat}(m,n,A) \\\\to_{\\\\mathbb{R}} \\mathrm{Mat}(l,n,A), \\\\; (X) \\, (Y) = X Y.$$$$
Lean4
/-- On square matrices, `Matrix.mulLeftLinearMap` and `LinearMap.mulLeft` coincide. -/
theorem mulLeftLinearMap_eq_mulLeft : mulLeftLinearMap m R = LinearMap.mulLeft R (A := Matrix m m A) :=
rfl
