Exact real polar angle #
The real instance uses Mathlib's principal complex argument in (-π, π], with angle zero at the
origin. This module keeps complex analysis out of executable scalar interfaces.
The real instance uses Mathlib's principal complex argument in (-π, π], with angle zero at the
origin. This module keeps complex analysis out of executable scalar interfaces.