vec_add

Mathlib.LinearAlgebra.Matrix.Vec

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

English

Vectorization commutes with finite sums: vec(sum_i A_i) = sum_i vec(A_i).

Русский

Векторизация commuting с суммой: vec(∑ A_i) = ∑ vec(A_i).

LaTeX

$$$$\operatorname{vec}\left(\sum_{i} A_i\right) = \sum_{i} \operatorname{vec}(A_i)$$$$

Lean4

@[simp]
theorem vec_add [Add R] (A B : Matrix m n R) : vec (A + B) = vec A + vec B :=
  rfl

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

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

Разделы

Аффилиация

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