exp_int_mul — Mathlib

English

For z ∈ ℂ and n ∈ ℤ, exp(nz) = exp(z)^n; the ordinary integer powers extend through the exponential.

Русский

Для комплексного z и целого числа n верно exp(nz) = exp(z)^n; целочисленные степени продолжают экспоненту.

LaTeX

$$$\\forall z \\in \\mathbb{C}, \\forall n \\in \\mathbb{Z}, \\\\ Exp(n z) = Exp(z)^n$$$

Lean4

theorem exp_int_mul (z : ℂ) (n : ℤ) : Complex.exp (n * z) = Complex.exp z ^ n :=
  by
  cases n
  · simp [exp_nat_mul]
  · simp [exp_add, add_mul, pow_add, exp_neg, exp_nat_mul]

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