ofReal_cpow — Mathlib

English

If x ≥ 0 is real and y is real, then the real power x^y considered as a complex number equals the complex power x^y with complex exponent.

Русский

Если x≥0 является действительным числом и y — действительное число, то вещественная степень x^y воспринятая как комплексное число равна комплексной степени x^y с комплексным показателем.

LaTeX

$$$x \ge 0 \Rightarrow ((x^{y} : \mathbb{R}) : \mathbb{C}) = (x : \mathbb{C})^{(y : \mathbb{C})}$$$

Lean4

theorem ofReal_cpow {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : ((x ^ y : ℝ) : ℂ) = (x : ℂ) ^ (y : ℂ) := by
  simp only [Real.rpow_def_of_nonneg hx, Complex.cpow_def, ofReal_eq_zero]; split_ifs <;> simp [Complex.ofReal_log hx]

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