exp_add_of_commute

Mathlib.Analysis.Normed.Algebra.MatrixExponential

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

← MathLib Explorer

English

If A and B commute, then exp(A + B) = exp(A) exp(B).

Русский

Если A и B коммутируют, то exp(A + B) = exp(A) exp(B).

LaTeX

$$$\\text{Commute}(A,B) \\Rightarrow \\exp(A+B) = \\exp(A) \\exp(B)$$$

Lean4

nonrec theorem exp_add_of_commute (A B : Matrix m m 𝔸) (h : Commute A B) : exp 𝕂 (A + B) = exp 𝕂 A * exp 𝕂 B :=
  open scoped Norms.Operator in exp_add_of_commute h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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