exp_one_pow

Mathlib.Analysis.SpecialFunctions.Pow.Real

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

English

For natural n, exp(1)^n = exp(n).

Русский

Для натурального n: exp(1)^n = exp(n).

LaTeX

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

Lean4

@[simp]
theorem exp_one_pow (n : ℕ) : exp 1 ^ n = exp n := by rw [← rpow_natCast, exp_one_rpow]

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

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

Разделы

Аффилиация

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