vec_sum — Mathlib

English

Vectorization commutes with finite sums of matrices indexed by a finite set: vec(∑_{i∈s} A_i) = ∑_{i∈s} vec(A_i).

Русский

Векторизация сумм по конечному индексу сохраняется: vec(∑_{i∈s} A_i) = ∑_{i∈s} vec(A_i).

LaTeX

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

Lean4

theorem vec_sum [AddCommMonoid R] (s : Finset ι) (A : ι → Matrix m n R) : vec (∑ i ∈ s, A i) = ∑ i ∈ s, vec (A i) :=
  by
  ext
  simp_rw [vec, Finset.sum_apply, vec, Matrix.sum_apply]

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