exp_conj

Mathlib.Analysis.Normed.Algebra.Exponential

URI: https://scilib.ai/kg/mathlib#NormedSpace.exp_conj

English

For a unit y, exp( y⁻¹ x y ) = y⁻¹ exp(x) y.

Русский

Для единичного элемента y: exp(y^{-1} x y) = y^{-1} exp(x) y.

LaTeX

$$$\\exp 𝕂 (y^{-1} x y) = y^{-1} \\exp 𝕂 x y$$$

Lean4

theorem exp_conj (y : 𝔸) (x : 𝔸) (hy : y ≠ 0) : exp 𝕂 (y * x * y⁻¹) = y * exp 𝕂 x * y⁻¹ :=
  exp_units_conj _ (Units.mk0 y hy) x

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

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

Разделы

Аффилиация

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