cpow_mul_ofReal_nonneg — Mathlib

English

Let x ∈ ℝ with x ≥ 0, y ∈ ℝ, and z ∈ ℂ. Then (x)^{yz} = (x^y)^z, using the standard complex extension of real-base powers.

Русский

Пусть x ∈ ℝ, x ≥ 0, y ∈ ℝ и z ∈ ℂ. Тогда x^{yz} = (x^y)^z через обычное комплексное продолжение вещественной степени.

LaTeX

$$$\\\\forall x \in \mathbb{R}, \ x \ge 0, \ \forall y \in \mathbb{R}, \forall z \in \\mathbb{C}: \ (x^{\, y z}) = (x^{\, y})^{\, z}.$$$

Lean4

theorem cpow_mul_ofReal_nonneg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) (z : ℂ) : (x : ℂ) ^ (↑y * z) = (↑(x ^ y) : ℂ) ^ z :=
  by
  rw [cpow_mul, ofReal_cpow hx]
  · rw [← ofReal_log hx, ← ofReal_mul, ofReal_im, neg_lt_zero]; exact Real.pi_pos
  · rw [← ofReal_log hx, ← ofReal_mul, ofReal_im]; exact Real.pi_pos.le

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