cpow_ofNat_mul' — Mathlib

English

For x ∈ ℂ, n ∈ ℕ with [n.AtLeastTwo], (-π < OfNat(n)·arg(x)) and (OfNat(n)·arg(x) ≤ π) hold, then x^(OfNat(n)·y) = (x^ofNat(n))^y for all y ∈ ℂ.

Русский

Пусть x ∈ ℂ, n ∈ ℕ, n ≥ 2, и выполняются (-π < n·arg(x)) и (n·arg(x) ≤ π). Тогда x^(n·y) = (x^n)^y для любого y ∈ ℂ.

LaTeX

$$$x^{(\mathrm{OfNat}(n) \cdot y)} = (x^{\mathrm{OfNat}(n)})^{y}$$$

Lean4

theorem cpow_ofNat_mul' {x : ℂ} {n : ℕ} [n.AtLeastTwo] (hlt : -π < OfNat.ofNat n * x.arg)
    (hle : OfNat.ofNat n * x.arg ≤ π) (y : ℂ) : x ^ (OfNat.ofNat n * y) = (x ^ ofNat(n)) ^ y :=
  cpow_nat_mul' hlt hle y

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