cpow_mul — Mathlib

English

Under the principal-branch constraint -π < Im(log x · y) ≤ π, x^(y z) = (x^y)^z.

Русский

При условии на мнимую часть log x · y, выполняющем -π < Im(log x · y) ≤ π, выполняется x^(y z) = (x^y)^z.

LaTeX

$$$$ x^{(y \cdot z)} = (x^{y})^{z} \quad \text{provided } -\pi < \operatorname{Im}(\log x \cdot y) \le \pi. $$$$

Lean4

theorem cpow_mul {x y : ℂ} (z : ℂ) (h₁ : -π < (log x * y).im) (h₂ : (log x * y).im ≤ π) : x ^ (y * z) = (x ^ y) ^ z :=
  by
  simp only [cpow_def]
  split_ifs <;> simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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