star_exp — Mathlib

English

The star operation commutes with the exponential: taking adjoints before or after exponentiation yields the same result.

Русский

Операция звезды сохраняется сквозь показатель экспоненты: star(exp x) = exp(star x).

LaTeX

$$$\\star(\\exp 𝕂 x) = \\exp 𝕂 (\\star x).$$$

Lean4

theorem star_exp [T2Space 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] (x : 𝔸) : star (exp 𝕂 x) = exp 𝕂 (star x) := by
  simp_rw [exp_eq_tsum, ← star_pow, ← star_inv_natCast_smul, ← tsum_star]

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