exp_nat_mul

Mathlib.Analysis.Complex.Exponential

URI: https://scilib.ai/kg/mathlib#Complex.exp_nat_mul

← MathLib Explorer

English

For z ∈ ℂ and integer n, exp(n z) = exp(z)^n.

Русский

Для комплексного z и целого n: exp(n z) = exp(z)^n.

LaTeX

$$$\\exp(n z) = (\\exp z)^n$$$

Lean4

theorem exp_nat_mul (x : ℂ) : ∀ n : ℕ, exp (n * x) = exp x ^ n
  | 0 => by rw [Nat.cast_zero, zero_mul, exp_zero, pow_zero]
  | Nat.succ n => by rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]

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

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

Разделы

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

Аффилиация

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