expUnitary_add — Mathlib

English

If a and b are self-adjoint and commute in A, then expUnitary(a+b) = expUnitary(a) expUnitary(b).

Русский

Если a и b — самоприводные и коммутируют в A, то expUnitary(a+b) = expUnitary(a) expUnitary(b).

LaTeX

$$$$\expUnitary(a+b) = \expUnitary(a) \expUnitary(b)$$$$

Lean4

theorem expUnitary_add {a b : selfAdjoint A} (h : Commute (a : A) (b : A)) :
    expUnitary (a + b) = expUnitary a * expUnitary b := by
  ext
  have hcomm : Commute (I • (a : A)) (I • (b : A)) :=
    by
    unfold Commute SemiconjBy
    simp only [h.eq, Algebra.smul_mul_assoc, Algebra.mul_smul_comm]
  simpa only [expUnitary_coe, AddSubgroup.coe_add, smul_add] using exp_add_of_commute hcomm

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