exp_conjTranspose — Mathlib

English

Another reiteration of the block-diagonal exponential property for a family v: exp(blockDiagonal' v) = blockDiagonal' (exp 𝕂 v).

Русский

Ещё одно утверждение для экспоненты блочной диагонали: exp(blockDiagonal' v) = blockDiagonal' (exp 𝕂 v).

LaTeX

$$$\\exp\\_\\mathbb{K}(\\operatorname{blockDiagonal}' v) = \\operatorname{blockDiagonal}'(\\exp\\_\\mathbb{K} v)$$$

Lean4

theorem exp_conjTranspose [StarRing 𝔸] [ContinuousStar 𝔸] (A : Matrix m m 𝔸) : exp 𝕂 Aᴴ = (exp 𝕂 A)ᴴ :=
  (star_exp A).symm

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