unit_length_complex_polar_angle

proveit.numbers.unit_length_complex_polar_angle(expr, \*, reductions=None)

Given an expression, expr, of the complex number polar form,

exp(i * theta),

or something obviously equivalent to this, where r is RealNonNeg and theta is Real under the given assumptions, return theta.

If expr is not exactly in this complex number polar form and ‘reductions’ is provided as a set, add to the ‘reductions’ set an equation that equates the exact form on the left with the original form on the right. This may be useful to use as ‘replacements’ in instantiations of theorems that employ the complex number polar form so it may perform proper reductions to the desired form. For example, if expr=1 is provided, the added reduction will be

exp(i * 0) = 1

Raise ValueError if the expr is not obviously equivalent to a complex number polar form.

Also see complex_polar_coordinates.