English
Let f be a map that preserves zero and respects addition (i.e., a linear-like map). Then applying f entrywise to the matrix with a in position (i, j) yields the matrix with f(a) in position (i, j).
Русский
Пусть f сохраняет ноль и аддитивен по точкам (аналог линейного отображения). Тогда применение f ко всей матрице, у которой в позиции (i, j) стоит a, даёт матрицу, в позиции (i, j) будет f(a).
LaTeX
$$$ (\mathrm{single}_{i j} a).map f = \mathrm{single}_{i j} (f a) $$$
Lean4
@[simp]
theorem map_single (i : m) (j : n) (a : α) {β : Type*} [Zero β] {F : Type*} [FunLike F α β] [ZeroHomClass F α β]
(f : F) : (single i j a).map f = single i j (f a) := by aesop (add unsafe unfold single)
