mathlib3

fa6e0243 - feat(analysis/special_functions/trigonometric/angle): `to_real` (#16007)

feat(analysis/special_functions/trigonometric/angle): `to_real` (#16007) Define `real.angle.to_real`, converting a `real.angle` to a real in the interval `Ioc (-π) π` (the same interval used by `complex.arg`), and prove some associated lemmas. This is the inverse operation to coercing the result of `complex.arg` to `real.angle`, and is also useful for converting between oriented and unoriented angles.