mathlib
mathlib copied to clipboard
Published
20 hours ago •
leanprover-community
leanprover-community
feat(analysis/special_functions/trigonometric/angle): `to_real`
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.
