exp_mem_unitary_of_mem_skewAdjoint

English

If x is skew-adjoint in a star-algebra, then exp(𝕂 x) is a unitary element.

Русский

Пусть x косо сопряжённый в звёздной алгебре; тогда exp(𝕂 x) является унитарным элементом.

LaTeX

$$$x \\in \\operatorname{skewAdjoint} 𝔸 \\;\\Rightarrow\\; \\exp 𝕂 x \\in \\operatorname{unitary} 𝔸$$$

Lean4

theorem exp_mem_unitary_of_mem_skewAdjoint [StarRing 𝔸] [ContinuousStar 𝔸] {x : 𝔸} (h : x ∈ skewAdjoint 𝔸) :
    exp 𝕂 x ∈ unitary 𝔸 := by
  rw [unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ← exp_add_of_commute (Commute.refl x).neg_left, ←
    exp_add_of_commute (Commute.refl x).neg_right, neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]

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