Polar angle of real coordinates

Complex logarithms need the argument of a point, in addition to real logarithms and square roots. Atan2 supplies this real-coordinate operation without requiring an ordering or an angle operation on complex numbers themselves. Floating-point instances follow the host library's signed-zero and branch-cut conventions.

class Atan2 (α : Type) : Type

Principal polar angle of the point (x, y), in radians.

• atan2 : α → α → α

  The argument order is y, x, as in the standard two-argument arctangent.

@[instance_reducible]

instance instAtan2Float : Atan2 Float

@[instance_reducible]

instance instAtan2Float32 : Atan2 Float32