vec_map

Mathlib.LinearAlgebra.Matrix.Vec

URI: https://scilib.ai/kg/mathlib#Matrix.vec_map

English

If A is a matrix and f a function, then vec(A.map f) equals f applied to each entry of vec(A).

Русский

Если A — матрица, а f — функция, то vec(A.map f) равно применению f к каждой компоненте vec(A).

LaTeX

$$$$\operatorname{vec}(A_{\text{map} f}) = f \circ \operatorname{vec}(A)$$$$

Lean4

theorem vec_map (A : Matrix m n R) (f : R → S) : vec (A.map f) = f ∘ vec A :=
  rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru