exp_nsmul

Mathlib.Analysis.Normed.Algebra.Exponential

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

← MathLib Explorer

English

For natural n, exp(n•x) = (exp x)^n.

Русский

Для натурального n выполняется exp(n•x) = (exp x)^n.

LaTeX

$$$\\exp 𝕂\\left(n \\cdot x\\right) = \\exp 𝕂(x)^n$$$

Lean4

theorem exp_nsmul (n : ℕ) (x : 𝔸) : exp 𝕂 (n • x) = exp 𝕂 x ^ n := by
  induction n with
  | zero => rw [zero_smul, pow_zero, exp_zero]
  | succ n ih => rw [succ_nsmul, pow_succ, exp_add_of_commute ((Commute.refl x).smul_left n), ih]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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