transpose_multiset_sum — Mathlib

English

The transpose distributes over sum in multisets of matrices.

Русский

Транспонирование распределяется по сумме в мультимножествах матриц.

LaTeX

$$$\sum^T_{s} = \left( \mathrm{map}(\mathrm{transpose}, s) \right).\sum$ for a multiset s of matrices.$$

Lean4

theorem transpose_multiset_sum [AddCommMonoid α] (s : Multiset (Matrix m n α)) : s.sumᵀ = (s.map transpose).sum :=
  (transposeAddEquiv m n α).toAddMonoidHom.map_multiset_sum s

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