English
The map operation applies a function to each entry of a matrix, producing a matrix with entries f(M_{ij}).
Русский
Операция map применяет функцию к каждому элементу матрицы, получая матрицу с элементами f(M_{ij}).
LaTeX
$$$(M.map\\ f)_{ij} = f(M_{ij})$$$
Lean4
/-- `M.map f` is the matrix obtained by applying `f` to each entry of the matrix `M`.
This is available in bundled forms as:
* `AddMonoidHom.mapMatrix`
* `LinearMap.mapMatrix`
* `RingHom.mapMatrix`
* `AlgHom.mapMatrix`
* `Equiv.mapMatrix`
* `AddEquiv.mapMatrix`
* `LinearEquiv.mapMatrix`
* `RingEquiv.mapMatrix`
* `AlgEquiv.mapMatrix`
-/
def map (M : Matrix m n α) (f : α → β) : Matrix m n β :=
of fun i j => f (M i j)
