pow_cpow_nat_inv — Mathlib

English

For x ∈ ℂ and n ∈ ℕ with n ≠ 0, (x^n)^(1/n) = x, provided arg(x) lies in the interval (−π/n, π/n).

Русский

Для x ∈ ℂ и n ∈ ℕ, n ≠ 0, (x^n)^(1/n) = x при условии, что arg(x) ∈ (−π/n, π/n].

LaTeX

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

Lean4

theorem pow_cpow_nat_inv {x : ℂ} {n : ℕ} (h₀ : n ≠ 0) (hlt : -(π / n) < x.arg) (hle : x.arg ≤ π / n) :
    (x ^ n) ^ (n⁻¹ : ℂ) = x :=
  by
  rw [← cpow_nat_mul', mul_inv_cancel₀ (Nat.cast_ne_zero.2 h₀), cpow_one]
  · rwa [← div_lt_iff₀' (Nat.cast_pos.2 h₀.bot_lt), neg_div]
  · rwa [← le_div_iff₀' (Nat.cast_pos.2 h₀.bot_lt)]

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