cpow_nat_mul' — Mathlib

English

For x ∈ ℂ, n ∈ ℕ with valid angle bounds, and y ∈ ℂ, x^(n·y) = (x^n)^y.

Русский

Для x ∈ ℂ, n ∈ ℕ при допустимых пределах аргумента и y ∈ ℂ верно x^(n·y) = (x^n)^y.

LaTeX

$$$x^{(n \cdot y)} = (x^{n})^{y}$$$

Lean4

/-- A version of `Complex.cpow_nat_mul` with RHS that matches `Complex.cpow_mul`.

The assumptions on the arguments are needed
because the equality fails, e.g., for `x = -I`, `n = 2`, `y = 1/2`. -/
theorem cpow_nat_mul' {x : ℂ} {n : ℕ} (hlt : -π < n * x.arg) (hle : n * x.arg ≤ π) (y : ℂ) :
    x ^ (n * y) = (x ^ n) ^ y :=
  cpow_int_mul' hlt hle y

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