exp_units_conj' — Mathlib

English

For U a unit (invertible matrix with inverse U^{-1}) and A any 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_units_conj' (U : (Matrix m m 𝔸)ˣ) (A : Matrix m m 𝔸) : exp 𝕂 (U⁻¹ * A * U) = U⁻¹ * exp 𝕂 A * U :=
  exp_units_conj 𝕂 U⁻¹ A

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