English
There is a canonical linear map that encodes matrix multiplication as a bilinear operation: mulLinearMap : Matrix l m A →ₗ[R] Matrix m n A →ₗ[R] Matrix l n A, with toFun(X) = (Y ↦ X · Y) and respecting addition and scalar multiplication.
Русский
Существует каноническая линейная карта, кодирующая умножение матриц как билинейную операцию: mulLinearMap : Matrix l m A →ₗ[R] Matrix m n A →ₗ[R] Matrix l n A, где toFun(X) = (Y ↦ X · Y) и сохраняет сложение и умножение на скаляры.
LaTeX
$$$$\\mathrm{mulLinearMap} : \\mathrm{Mat}(l,m,A) \\to_{R} \\mathrm{Mat}(m,n,A) \\to_{R} \\mathrm{Mat}(l,n,A), \\; X \\mapsto (Y \\mapsto X Y).$$$$
Lean4
/-- A version of `LinearMap.mul` for matrix multiplication. -/
@[simps!]
def mulLinearMap : Matrix l m A →ₗ[R] Matrix m n A →ₗ[R] Matrix l n A
where
toFun := mulLeftLinearMap n R
map_add' _ _ := LinearMap.ext fun _ => Matrix.add_mul _ _ _
map_smul' _ _ := LinearMap.ext fun _ => Matrix.smul_mul _ _ _
