English
Let f be a bijection between the coefficient types α and β. Then applying f entrywise to m×n matrices gives a bijection between matrices with entries from α and matrices with entries from β; the inverse is obtained by applying f^{-1} entrywise.
Русский
Пусть f : α ≃ β — биекция. Тогда отображение, которое применяет f ко всем элементам матрицы размером m×n, устанавливает биективное соответствие между матрицами над α и матрицами над β; обратное отображение получается применением f^{-1} к каждому элементу.
LaTeX
$$$\\text{For any } f:\\alpha \\simeq \\beta, \\ \\mathrm{Mat}_{m\\times n}(\\alpha) \\cong \\mathrm{Mat}_{m\\times n}(\\beta)\\text{ via } (M)_{ij} \\mapsto f(M_{ij}), \\text{ with inverse } (N)_{ij} \\mapsto f^{-1}(N_{ij}).$$$
Lean4
/-- The `Equiv` between spaces of matrices induced by an `Equiv` between their
coefficients. This is `Matrix.map` as an `Equiv`. -/
@[simps apply]
def mapMatrix (f : α ≃ β) : Matrix m n α ≃ Matrix m n β
where
toFun M := M.map f
invFun M := M.map f.symm
left_inv _ := Matrix.ext fun _ _ => f.symm_apply_apply _
right_inv _ := Matrix.ext fun _ _ => f.apply_symm_apply _
