English
The construction mapMatrix is linear in the map being applied; it is a linear map in that parameter.
Русский
Конструкция mapMatrix линейна по отображению, которое она применяет; она образует линейное отображение по этому параметру.
LaTeX
$$$\\mathrm{mapMatrixLinear} : (\\alpha \\to_{\\sigma} \\beta) \\\\to_L[A] (\\mathrm{Matrix} m n \\alpha \\to_{\\sigma} \\mathrm{Matrix} m n \\beta)$$$
Lean4
/-- `LinearMap.mapMatrix` is itself linear in the map being applied.
Alternative, this is `Matrix.map` as a bilinear map. -/
@[simps]
def mapMatrixLinear [Semiring A] [Module A β] [SMulCommClass S A β] :
(α →ₛₗ[σᵣₛ] β) →ₗ[A] (Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β)
where
toFun := mapMatrix
map_add' := mapMatrix_add
map_smul' := mapMatrix_smul
