conjTranspose_multiset_sum — Mathlib

English

For a multiset of matrices s, the conjugate transpose distributes over the multiset sum: sum^H = sum (M^H) over the multiset.

Русский

Для мультисета матриц s распределение сопряжённого транспонирования по сумме мультисета: сумма^H = сумма (M^H).

LaTeX

$$$ s.sum^H = (s.map conjTranspose).sum $$$

Lean4

theorem conjTranspose_multiset_sum [AddCommMonoid α] [StarAddMonoid α] (s : Multiset (Matrix m n α)) :
    s.sumᴴ = (s.map conjTranspose).sum :=
  (conjTransposeAddEquiv m n α).toAddMonoidHom.map_multiset_sum s

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