exp_conj' — Mathlib

English

For U a unit and A a matrix, exp(𝕂, U^{-1} A U) = U^{-1} exp(𝕂, A) U.

Русский

Для единицы U и любой матрицы A выполняется 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

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