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 x y^{-1} ) = y exp(x) y^{-1}.

Русский

Для единичного элемента y ∈ 𝔸 выполняется exp(y x y^{-1}) = y exp(x) y^{-1}.

LaTeX

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

Lean4

theorem exp_units_conj (y : 𝔸ˣ) (x : 𝔸) : exp 𝕂 (y * x * ↑y⁻¹ : 𝔸) = y * exp 𝕂 x * ↑y⁻¹ :=
  exp_smul _ (ConjAct.toConjAct y) x

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

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

Разделы

Аффилиация

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