English
An additive equivalence f: α ≃+ β induces an additive equivalence between matrix spaces: MapMatrix preserves structure by M ↦ M.map f, with inverse M ↦ M.map f.symm.
Русский
Аддитивная эквивалентность f: α ≃+ β порождает аддитивную эквивалентность между пространствами матриц: M ↦ M.map f и обратное M ↦ M.map f.symm.
LaTeX
$$$\\text{Let } f:\\alpha \\simeq_+ \\beta.\\ \\mathrm{AddEquiv.mapMatrix}(f) : \\mathrm{Mat}_{m\\times n}(\\alpha) \\simeq_+ \\mathrm{Mat}_{m\\times n}(\\beta)$ with $ (\\mathrm{mapMatrix}(f))(M) = M.map f$ and inverse $ (M) \\mapsto M.map f.symm$.$$
Lean4
/-- The `AddEquiv` between spaces of matrices induced by an `AddEquiv` between their
coefficients. This is `Matrix.map` as an `AddEquiv`. -/
@[simps apply]
def mapMatrix (f : α ≃+ β) : Matrix m n α ≃+ Matrix m n β :=
{ f.toEquiv.mapMatrix with
toFun := fun M => M.map f
invFun := fun M => M.map f.symm
map_add' := Matrix.map_add f (map_add f) }
