English
The map that sends a coefficient homomorphism to a matrix homomorphism preserves addition and zero: (f+g).mapMatrix = f.mapMatrix + g.mapMatrix, and 0 maps to 0.
Русский
Отображение, переводящее гомоморфизм коэффициентов в гомоморфизм матриц, сохраняет сложение и ноль: (f+g).mapMatrix = f.mapMatrix + g.mapMatrix и 0 идёт в 0.
LaTeX
$$$ (f+g).mapMatrix = f.mapMatrix + g.mapMatrix, \\quad 0.mapMatrix = 0 $$$
Lean4
/-- The `AddMonoidHom` between spaces of matrices induced by an `AddMonoidHom` between their
coefficients. This is `Matrix.map` as an `AddMonoidHom`. -/
@[simps]
def mapMatrix (f : α →+ β) : Matrix m n α →+ Matrix m n β
where
toFun M := M.map f
map_zero' := Matrix.map_zero f f.map_zero
map_add' := Matrix.map_add f f.map_add
