transpose_sum — Mathlib

English

Transpose commutes with finite sums: the transpose of a finite sum equals the sum of transposes.

Русский

Транспонирование коммутирует с конечной суммой: транспонирование суммы равняется сумме транспонированных элементов.

LaTeX

$$$\left( \sum_{i \in s} M_i \right)^T = \sum_{i\in s} M_i^T$ for finite index set s.$$

Lean4

theorem transpose_sum [AddCommMonoid α] {ι : Type*} (s : Finset ι) (M : ι → Matrix m n α) :
    (∑ i ∈ s, M i)ᵀ = ∑ i ∈ s, (M i)ᵀ :=
  map_sum (transposeAddEquiv m n α) _ s

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