exp

Mathlib.Analysis.Normed.Algebra.MatrixExponential

URI: https://scilib.ai/kg/mathlib#Matrix.IsSymm.exp

English

The exponential of the transpose equals the transpose of the exponential: exp(A^T) = (exp A)^T.

Русский

Экспонента транспонирования равна транспонированию экспоненты: exp(A^T) = (exp A)^T.

LaTeX

$$$\\exp(A^{T}) = (\\exp(A))^{T}$$$

Lean4

theorem exp {A : Matrix m m 𝔸} (h : A.IsSymm) : (exp 𝕂 A).IsSymm :=
  (exp_transpose _ _).symm.trans <| congr_arg _ h

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

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

Разделы

Аффилиация

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