cpow_int_mul' — Mathlib

English

If -π < n·arg(x) ≤ π, then x^(n·y) = (x^n)^y for any y ∈ ℂ.

Русский

Если -π < n·arg(x) ≤ π, то x^(n·y) = (x^n)^y для любого y ∈ ℂ.

LaTeX

$$$x^{(n \cdot y)} = (x^{n})^{y}$ при -\pi < n \arg(x) ≤ \pi$$

Lean4

/-- A version of `Complex.cpow_int_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_int_mul' {x : ℂ} {n : ℤ} (hlt : -π < n * x.arg) (hle : n * x.arg ≤ π) (y : ℂ) :
    x ^ (n * y) = (x ^ n) ^ y := by
  rw [mul_comm] at hlt hle
  rw [cpow_mul, cpow_intCast] <;> simpa [log_im]

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