sq_cpow_two_inv — Mathlib

English

For x ∈ ℂ and n ∈ ℕ with [n.AtLeastTwo], (x ^ ofNat(n))^(1/n) = x.

Русский

Для x ∈ ℂ и n ∈ ℕ, с n ≥ 2, (x^{ofNat(n)})^{1/n} = x.

LaTeX

$$$\bigl(x^{\mathrm{ofNat}(n)}\bigr)^{\frac{1}{n}} = x$$$

Lean4

/-- See also `Complex.pow_cpow_ofNat_inv` for a version that also works for `x * I`, `0 ≤ x`. -/
theorem sq_cpow_two_inv {x : ℂ} (hx : 0 < x.re) : (x ^ (2 : ℕ)) ^ (2⁻¹ : ℂ) = x :=
  pow_cpow_ofNat_inv (neg_pi_div_two_lt_arg_iff.2 <| .inl hx) (arg_le_pi_div_two_iff.2 <| .inl hx.le)

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