conjTranspose_sum — Mathlib

English

For a finite index set s and family of matrices M_i, the conjugate transpose commutes with finite sums: (∑ i∈s M_i)^H = ∑ i∈s M_i^H.

Русский

Для конечного множества индексов s и семейства матриц M_i сопряжённое транспонирование коммутирует с конечной суммой: (∑ i∈s M_i)^H = ∑ i∈s M_i^H.

LaTeX

$$$ \left( \sum_{i \in s} M_i \right)^H = \sum_{i \in s} M_i^H $$$

Lean4

theorem conjTranspose_sum [AddCommMonoid α] [StarAddMonoid α] {ι : Type*} (s : Finset ι) (M : ι → Matrix m n α) :
    (∑ i ∈ s, M i)ᴴ = ∑ i ∈ s, (M i)ᴴ :=
  map_sum (conjTransposeAddEquiv m n α) _ s

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