exp_left

Mathlib.Analysis.Normed.Algebra.Exponential

URI: https://scilib.ai/kg/mathlib#Commute.exp_left

English

If x commutes with y, then exp(x) commutes with y.

Русский

Если x коммутирует с y, то exp(x) коммутирует с y.

LaTeX

$$Commute x y → Commute (\\exp 𝕂 x) y$$

Lean4

theorem _root_.Commute.exp_left [T2Space 𝔸] {x y : 𝔸} (h : Commute x y) : Commute (exp 𝕂 x) y :=
  (h.symm.exp_right 𝕂).symm

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

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

Разделы

Аффилиация

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