pow_cpow_ofNat_inv — Mathlib

English

For x ∈ ℂ and n ∈ ℕ with n ≠ 0 and −(π/n) < x.arg ≤ π/n, we have (x^n)^{1/n} = x.

Русский

Для x ∈ ℂ и n ∈ ℕ с n ≠ 0 и −(π/n) < arg(x) ≤ π/n выполняется (x^n)^{1/n} = x.

LaTeX

$$$\bigl(x^{n}\bigr)^{\frac{1}{n}} = x \quad (n \neq 0, \ -\frac{\pi}{n} < \arg(x) \le \frac{\pi}{n})$$$

Lean4

theorem pow_cpow_ofNat_inv {x : ℂ} {n : ℕ} [n.AtLeastTwo] (hlt : -(π / OfNat.ofNat n) < x.arg)
    (hle : x.arg ≤ π / OfNat.ofNat n) : (x ^ ofNat(n)) ^ ((OfNat.ofNat n : ℂ)⁻¹) = x :=
  pow_cpow_nat_inv (NeZero.ne n) hlt hle

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