matrix_conjTranspose — Mathlib

English

The conjugate transpose of the tsum equals the tsum of conjugate transposes, under suitable conditions.

Русский

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

LaTeX

$$$\\text{transpose}(\\sum'_{L} f) = \\sum'_{L} f^H$$$

Lean4

theorem matrix_conjTranspose [StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} (hf : Summable f L) :
    Summable (fun x => (f x)ᴴ) L :=
  hf.hasSum.matrix_conjTranspose.summable

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