English
Applying a function to every entry of a matrix is implemented by a map operation: M.map f has entries (M.map f)_{ij} = f(M_{ij}).
Русский
Преобразование каждой величины матрицы через функцию применяется по всем элементам: (M.map f)_{ij} = f(M_{ij}).
LaTeX
$$$(M.map\\ f)_{ij} = f(M_{ij})$$$
Lean4
/-- Cast a function into a matrix.
The two sides of the equivalence are definitionally equal types. We want to use an explicit cast
to distinguish the types because `Matrix` has different instances to pi types (such as `Pi.mul`,
which performs elementwise multiplication, vs `Matrix.mul`).
If you are defining a matrix, in terms of its entries, use `of (fun i j ↦ _)`. The
purpose of this approach is to ensure that terms of the form `(fun i j ↦ _) * (fun i j ↦ _)` do not
appear, as the type of `*` can be misleading.
-/
def of : (m → n → α) ≃ Matrix m n α :=
Equiv.refl _
