exp_one_rpow

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Real.exp_one_rpow

English

For any real x, exp(1) ^ x = exp(x).

Русский

Для любого x ∈ ℝ: exp(1) ^ x = exp(x).

LaTeX

$$$$ \\exp(1)^x = \\exp(x). $$$$

Lean4

@[simp]
theorem exp_one_rpow (x : ℝ) : exp 1 ^ x = exp x := by rw [← exp_mul, one_mul]

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

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

Разделы

Аффилиация

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