exp_units_conj — Mathlib

English

If U is an invertible matrix then exp(𝕂, U A U^{-1}) = U exp(𝕂, A) U^{-1}.

Русский

Если U обратима, то экспонента ведёт себя при подобии: exp(U A U^{-1}) = U exp(A) U^{-1}.

LaTeX

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

Lean4

nonrec theorem exp_units_conj (U : (Matrix m m 𝔸)ˣ) (A : Matrix m m 𝔸) : exp 𝕂 (U * A * U⁻¹) = U * exp 𝕂 A * U⁻¹ :=
  open scoped Norms.Operator in exp_units_conj _ U A

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