exp_transpose

Mathlib.Analysis.Normed.Algebra.MatrixExponential

URI: https://scilib.ai/kg/mathlib#Matrix.exp_transpose

English

If A is Hermitian, then exp(A) is Hermitian as well.

Русский

Если A эрмитова, то exp(A) также эрмитова.

LaTeX

$$$A \\text{ Hermitian} \\Rightarrow \\exp(A) \\text{ Hermitian}$$$

Lean4

theorem exp_transpose (A : Matrix m m 𝔸) : exp 𝕂 Aᵀ = (exp 𝕂 A)ᵀ := by
  simp_rw [exp_eq_tsum, transpose_tsum, transpose_smul, transpose_pow]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru