conjTranspose_tsum — Mathlib

English

The conjTranspose of the tsum equals tsum of conjTransposes.

Русский

Сопряжённо-транспонированная сумма равна сумме сопряжённых транспонированных.

LaTeX

$$$\\operatorname{conjTranspose}(\\sum'_{L} f) = \\sum'_{L} f^H$$$

Lean4

theorem conjTranspose_tsum [StarAddMonoid R] [ContinuousStar R] [T2Space R] {f : X → Matrix m n R} :
    (∑'[L] x, f x)ᴴ = ∑'[L] x, (f x)ᴴ :=
  Function.LeftInverse.map_tsum f (g := conjTransposeAddEquiv m n R) continuous_id.matrix_conjTranspose
    continuous_id.matrix_conjTranspose conjTranspose_conjTranspose

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