English
Same principle as above, emphasizing compatibility of entry projections with the induced matrix map for AddEquiv.
Русский
Та же идея: совместимость проекций на элементы с индуцированным отображением матриц для AddEquiv.
LaTeX
$$$(\\text{entryAddHom } β i j).comp (AddHomClass.toAddHom f.mapMatrix) = (f : AddHom α β).comp (entryAddHom _ i j)$$$
Lean4
/-- The `LinearMap` between spaces of matrices induced by a `LinearMap` between their
coefficients. This is `Matrix.map` as a `LinearMap`. -/
@[simps]
def mapMatrix (f : α →ₛₗ[σᵣₛ] β) : Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β
where
toFun M := M.map f
map_add' := Matrix.map_add f f.map_add
map_smul' r := Matrix.map_smulₛₗ f _ r (f.map_smulₛₗ r)
