exp_nsmul' — Mathlib

English

For complex x, a, p ∈ ℂ and n ∈ ℕ, exp(a n x / p) = exp(a x / p)^n.

Русский

Для комплексных x, a, p ∈ ℂ и n ∈ ℕ: exp(a n x / p) = exp(a x / p)^n.

LaTeX

$$$\\exp\\left(\\frac{a n x}{p}\\right) = \\left(\\exp\\left(\\frac{a x}{p}\\right)\\right)^n$$$

Lean4

/-- This is a useful version of `exp_nsmul` for q-expansions of modular forms. -/
theorem exp_nsmul' (x a p : ℂ) (n : ℕ) : exp (a * n * x / p) = exp (a * x / p) ^ n :=
  by
  rw [← Complex.exp_nsmul]
  ring_nf

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