circle): `real.angle.exp_map_circle` (#11627)

Commit

4 years ago

feat(analysis/special_functions/complex/circle): `real.angle.exp_map_circle` (#11627) Add a version of `exp_map_circle` that applies to a `real.angle` argument.

Author

jsm28

Parents

f5b11ad5

mathlib 033dd3c5 - feat(analysis/special_functions/complex/circle): `real.angle.exp_map_circle` (#11627)

mathlib
033dd3c5 - feat(analysis/special_functions/complex/circle): `real.angle.exp_map_circle` (#11627)