# mathlib3documentation

analysis.special_functions.pow.complex

# Power function on ℂ#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[protected, instance]
noncomputable def complex.has_pow  :
Equations
@[simp]
theorem complex.cpow_eq_pow (x y : ) :
x.cpow y = x ^ y
theorem complex.cpow_def (x y : ) :
x ^ y = ite (x = 0) (ite (y = 0) 1 0) (cexp * y))
theorem complex.cpow_def_of_ne_zero {x : } (hx : x 0) (y : ) :
x ^ y = cexp * 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₁ : -real.pi < * 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⁻¹
@[simp, norm_cast]
theorem complex.cpow_nat_cast (x : ) (n : ) :
x ^ n = x ^ n
@[simp]
theorem complex.cpow_two (x : ) :
x ^ 2 = x ^ 2
@[simp, norm_cast]
theorem complex.cpow_int_cast (x : ) (n : ) :
x ^ n = x ^ n
theorem complex.cpow_nat_inv_pow (x : ) {n : } (hn : n 0) :
(x ^ (n)⁻¹) ^ n = x
theorem complex.mul_cpow_of_real_nonneg {a b : } (ha : 0 a) (hb : 0 b) (r : ) :
(a * b) ^ r = a ^ r * b ^ r
theorem complex.inv_cpow_eq_ite (x n : ) :
x⁻¹ ^ n = ite (x.arg = real.pi) ( (x ^ n)⁻¹) (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)⁻¹ = ite (x.arg = real.pi) ( (x⁻¹ ^ n)) (x⁻¹ ^ n)

complex.inv_cpow_eq_ite with the ite on the other side.

theorem complex.conj_cpow_eq_ite (x n : ) :
x ^ n = ite (x.arg = real.pi) (x ^ n) ( (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)

## Tactic extensions for complex powers #

theorem norm_num.cpow_pos (a b : ) (b' : ) (c : ) (hb : b = b') (h : a ^ b' = c) :
a ^ b = c
theorem norm_num.cpow_neg (a b : ) (b' : ) (c c' : ) (hb : b = b') (h : a ^ b' = c) (hc : c⁻¹ = c') :
a ^ -b = c'
meta def norm_num.prove_rpow' (pos neg zero : name) (α β one a b : expr) :

Generalized version of prove_cpow, prove_nnrpow, prove_ennrpow.

Evaluate complex.cpow a b where a is a rational numeral and b is an integer.

Evaluates expressions of the form cpow a b and a ^ b in the special case where b is an integer and a is a positive rational (so it's really just a rational power).