exp_conj — Mathlib

English

If hy is IsUnit U, exp(𝕂, U^{-1} A U) = U^{-1} exp(𝕂, A) U.

Русский

Если U единичный элемент, то exp(U^{-1} A U) = U^{-1} exp(A) U.

LaTeX

$$$\exp_{\mathbb{K}}(U^{-1} A U) = U^{-1} \exp_{\mathbb{K}}(A) U.$$$

Lean4

theorem exp_conj (U : Matrix m m 𝔸) (A : Matrix m m 𝔸) (hy : IsUnit U) : exp 𝕂 (U * A * U⁻¹) = U * exp 𝕂 A * U⁻¹ :=
  let ⟨u, hu⟩ := hy
  hu ▸ by simpa only [Matrix.coe_units_inv] using exp_units_conj 𝕂 u A

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