exp_units_conj'

Mathlib.Analysis.Normed.Algebra.Exponential

URI: https://scilib.ai/kg/mathlib#NormedSpace.exp_units_conj'

English

For a unit y, exp(y^{-1} x y) = y^{-1} 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_units_conj' (y : 𝔸ˣ) (x : 𝔸) : exp 𝕂 (↑y⁻¹ * x * y) = ↑y⁻¹ * exp 𝕂 x * y :=
  exp_units_conj _ _ _

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

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

Разделы

Аффилиация

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