exp_neg

Mathlib.Analysis.Normed.Algebra.Exponential

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

English

For z ∈ ℤ, exp(z • x) = (exp 𝕂 x)^z.

Русский

Для целого z выполняется exp(z • x) = (exp 𝕂 x)^z.

LaTeX

$$$\\exp 𝕂 (z \\cdot x) = \\exp 𝕂 x^{\,z}$$$

Lean4

theorem exp_neg (x : 𝔸) : exp 𝕂 (-x) = (exp 𝕂 x)⁻¹ :=
  exp_neg_of_mem_ball <| (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

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

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

Разделы

Аффилиация

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