rpow_mul — Mathlib

English

Let x ≥ 0 and y,z ∈ ℝ. Then x^{yz} = (x^y)^z.

Русский

Пусть x ≥ 0 и y,z ∈ ℝ. Тогда x^{yz} = (x^y)^z.

LaTeX

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

Lean4

theorem rpow_mul {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ (y * z) = (x ^ y) ^ z := by
  rw [← Complex.ofReal_inj, Complex.ofReal_cpow (rpow_nonneg hx _), Complex.ofReal_cpow hx, Complex.ofReal_mul,
      Complex.cpow_mul, Complex.ofReal_cpow hx] <;>
    simp only [(Complex.ofReal_mul _ _).symm, (Complex.ofReal_log hx).symm, Complex.ofReal_im, neg_lt_zero, pi_pos,
      le_of_lt pi_pos]

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