Power function on ℂ
#
We construct the power functions x ^ y
, where x
and y
are complex numbers.
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
.
Instances For
Equations
- Complex.instPow = { pow := Complex.cpow }
@[simp]
@[simp]
theorem
Complex.cpow_ofNat_mul'
{x : ℂ}
{n : ℕ}
[n.AtLeastTwo]
(hlt : -Real.pi < OfNat.ofNat n * x.arg)
(hle : OfNat.ofNat n * x.arg ≤ Real.pi)
(y : ℂ)
:
theorem
Complex.pow_cpow_ofNat_inv
{x : ℂ}
{n : ℕ}
[n.AtLeastTwo]
(hlt : -(Real.pi / OfNat.ofNat n) < x.arg)
(hle : x.arg ≤ Real.pi / OfNat.ofNat n)
: