# Power function on ℂ#

We construct the power functions x ^ y, where x and y are complex numbers.

noncomputable def Complex.cpow (x : ) (y : ) :

The complex power function x ^ y, given by x ^ y = exp(y log x) (where log is the principal determination of the logarithm), unless x = 0 where one sets 0 ^ 0 = 1 and 0 ^ y = 0 for y ≠ 0.

Equations
Instances For
noncomputable instance Complex.instPow :
Equations
@[simp]
theorem Complex.cpow_eq_pow (x : ) (y : ) :
x.cpow y = x ^ y
theorem Complex.cpow_def (x : ) (y : ) :
x ^ y = if x = 0 then if y = 0 then 1 else 0 else Complex.exp ( * y)
theorem Complex.cpow_def_of_ne_zero {x : } (hx : x 0) (y : ) :
x ^ y = Complex.exp ( * y)
@[simp]
theorem Complex.cpow_zero (x : ) :
x ^ 0 = 1
@[simp]
theorem Complex.cpow_eq_zero_iff (x : ) (y : ) :
x ^ y = 0 x = 0 y 0
@[simp]
theorem Complex.zero_cpow {x : } (h : x 0) :
0 ^ x = 0
theorem Complex.zero_cpow_eq_iff {x : } {a : } :
0 ^ x = a x 0 a = 0 x = 0 a = 1
theorem Complex.eq_zero_cpow_iff {x : } {a : } :
a = 0 ^ x x 0 a = 0 x = 0 a = 1
@[simp]
theorem Complex.cpow_one (x : ) :
x ^ 1 = x
@[simp]
theorem Complex.one_cpow (x : ) :
1 ^ x = 1
theorem Complex.cpow_add {x : } (y : ) (z : ) (hx : x 0) :
x ^ (y + z) = x ^ y * x ^ z
theorem Complex.cpow_mul {x : } {y : } (z : ) (h₁ : < ( * y).im) (h₂ : ( * y).im Real.pi) :
x ^ (y * z) = (x ^ y) ^ z
theorem Complex.cpow_neg (x : ) (y : ) :
x ^ (-y) = (x ^ y)⁻¹
theorem Complex.cpow_sub {x : } (y : ) (z : ) (hx : x 0) :
x ^ (y - z) = x ^ y / x ^ z
theorem Complex.cpow_neg_one (x : ) :
x ^ (-1) = x⁻¹
theorem Complex.cpow_int_mul (x : ) (n : ) (y : ) :
x ^ (n * y) = (x ^ y) ^ n

See also Complex.cpow_int_mul'.

theorem Complex.cpow_mul_int (x : ) (y : ) (n : ) :
x ^ (y * n) = (x ^ y) ^ n
theorem Complex.cpow_nat_mul (x : ) (n : ) (y : ) :
x ^ (n * y) = (x ^ y) ^ n
theorem Complex.cpow_ofNat_mul (x : ) (n : ) [n.AtLeastTwo] (y : ) :
x ^ ( * y) = (x ^ y) ^

See Note [no_index around OfNat.ofNat]

theorem Complex.cpow_mul_nat (x : ) (y : ) (n : ) :
x ^ (y * n) = (x ^ y) ^ n
theorem Complex.cpow_mul_ofNat (x : ) (y : ) (n : ) [n.AtLeastTwo] :
x ^ (y * ) = (x ^ y) ^

See Note [no_index around OfNat.ofNat]

@[simp]
theorem Complex.cpow_natCast (x : ) (n : ) :
x ^ n = x ^ n
@[deprecated Complex.cpow_natCast]
theorem Complex.cpow_nat_cast (x : ) (n : ) :
x ^ n = x ^ n

Alias of Complex.cpow_natCast.

@[simp]
theorem Complex.cpow_ofNat (x : ) (n : ) [n.AtLeastTwo] :
x ^ = x ^

See Note [no_index around OfNat.ofNat]

theorem Complex.cpow_two (x : ) :
x ^ 2 = x ^ 2
@[simp]
theorem Complex.cpow_intCast (x : ) (n : ) :
x ^ n = x ^ n
@[deprecated Complex.cpow_intCast]
theorem Complex.cpow_int_cast (x : ) (n : ) :
x ^ n = x ^ n

Alias of Complex.cpow_intCast.

@[simp]
theorem Complex.cpow_nat_inv_pow (x : ) {n : } (hn : n 0) :
(x ^ (n)⁻¹) ^ n = x
@[simp]
theorem Complex.cpow_ofNat_inv_pow (x : ) (n : ) [n.AtLeastTwo] :
(x ^ ()⁻¹) ^ = x

See Note [no_index around OfNat.ofNat]

theorem Complex.cpow_int_mul' {x : } {n : } (hlt : < n * x.arg) (hle : n * x.arg Real.pi) (y : ) :
x ^ (n * y) = (x ^ n) ^ y

A version of Complex.cpow_int_mul with RHS that matches Complex.cpow_mul.

The assumptions on the arguments are needed because the equality fails, e.g., for x = -I, n = 2, y = 1/2.

theorem Complex.cpow_nat_mul' {x : } {n : } (hlt : < n * x.arg) (hle : n * x.arg Real.pi) (y : ) :
x ^ (n * y) = (x ^ n) ^ y

A version of Complex.cpow_nat_mul with RHS that matches Complex.cpow_mul.

The assumptions on the arguments are needed because the equality fails, e.g., for x = -I, n = 2, y = 1/2.

theorem Complex.cpow_ofNat_mul' {x : } {n : } [n.AtLeastTwo] (hlt : < * x.arg) (hle : * x.arg Real.pi) (y : ) :
x ^ ( * y) = (x ^ ) ^ y
theorem Complex.pow_cpow_nat_inv {x : } {n : } (h₀ : n 0) (hlt : -(Real.pi / n) < x.arg) (hle : x.arg Real.pi / n) :
(x ^ n) ^ (n)⁻¹ = x
theorem Complex.pow_cpow_ofNat_inv {x : } {n : } [n.AtLeastTwo] (hlt : -() < x.arg) (hle : x.arg ) :
(x ^ ) ^ ()⁻¹ = x
theorem Complex.sq_cpow_two_inv {x : } (hx : 0 < x.re) :
(x ^ 2) ^ 2⁻¹ = x

See also Complex.pow_cpow_ofNat_inv for a version that also works for x * I, 0 ≤ x.

theorem Complex.mul_cpow_ofReal_nonneg {a : } {b : } (ha : 0 a) (hb : 0 b) (r : ) :
(a * b) ^ r = a ^ r * b ^ r
theorem Complex.natCast_mul_natCast_cpow (m : ) (n : ) (s : ) :
(m * n) ^ s = m ^ s * n ^ s
theorem Complex.natCast_cpow_natCast_mul (n : ) (m : ) (z : ) :
n ^ (m * z) = (n ^ m) ^ z
theorem Complex.inv_cpow_eq_ite (x : ) (n : ) :
x⁻¹ ^ n = if x.arg = Real.pi then () (x ^ () n)⁻¹ else (x ^ n)⁻¹
theorem Complex.inv_cpow (x : ) (n : ) (hx : x.arg Real.pi) :
x⁻¹ ^ n = (x ^ n)⁻¹
theorem Complex.inv_cpow_eq_ite' (x : ) (n : ) :
(x ^ n)⁻¹ = if x.arg = Real.pi then () (x⁻¹ ^ () n) else x⁻¹ ^ n

Complex.inv_cpow_eq_ite with the ite on the other side.

theorem Complex.conj_cpow_eq_ite (x : ) (n : ) :
() x ^ n = if x.arg = Real.pi then x ^ n else () (x ^ () n)
theorem Complex.conj_cpow (x : ) (n : ) (hx : x.arg Real.pi) :
() x ^ n = () (x ^ () n)
theorem Complex.cpow_conj (x : ) (n : ) (hx : x.arg Real.pi) :
x ^ () n = () (() x ^ n)