exp_conj'

Mathlib.Analysis.Normed.Algebra.Exponential

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

English

If y ≠ 0, exp 𝕂 (y x y^{-1}) = y exp 𝕂 x y^{-1}.

Русский

Если y ≠ 0, exp 𝕂 (y x y^{-1}) = y exp 𝕂 x y^{-1}.

LaTeX

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

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