English
The matrix-map induced by the identity on the coefficients is the identity map on matrices.
Русский
Отображение матриц, индуцируемое тождественным отображением на коэффициентах, является тождественным отображением на матрицах.
LaTeX
$$$(\mathrm{RingHom.id}_\alpha).mapMatrix = \mathrm{RingHom.id}_{\mathrm{Matrix}_{m\times m}(\alpha)}$$$
Lean4
/-- The `RingHom` between spaces of square matrices induced by a `RingHom` between their
coefficients. This is `Matrix.map` as a `RingHom`. -/
@[simps]
def mapMatrix (f : α →+* β) : Matrix m m α →+* Matrix m m β :=
{ f.toAddMonoidHom.mapMatrix with
toFun := fun M => M.map f
map_one' := by simp
map_mul' := fun _ _ => Matrix.map_mul }
