English
The identity RingEquiv on α yields the identity RingEquiv on matrices: RingEquiv.refl.mapMatrix = RingEquiv.refl (Matrix m m α).
Русский
Тождественный RingEquiv на α порождает тождественный RingEquiv на матрицах: RingEquiv.refl.mapMatrix = RingEquiv.refl (Matrix m m α).
LaTeX
$$$\text{RingEquiv.refl.mapMatrix} = \text{RingEquiv.refl} (\mathrm{Matrix}_{m\times m}(\alpha))$$$
Lean4
/-- The `RingEquiv` between spaces of square matrices induced by a `RingEquiv` between their
coefficients. This is `Matrix.map` as a `RingEquiv`. -/
@[simps apply]
def mapMatrix (f : α ≃+* β) : Matrix m m α ≃+* Matrix m m β :=
{ f.toRingHom.mapMatrix,
f.toAddEquiv.mapMatrix with
toFun := fun M => M.map f
invFun := fun M => M.map f.symm }
