mathlib3
2364a091 - feat(analysis/complex/circle): `exp_map_circle_neg` (#11889)

Commit
3 years ago
feat(analysis/complex/circle): `exp_map_circle_neg` (#11889) Add the lemma `exp_map_circle_neg`, similar to other lemmas for `exp_map_circle` that are already present.
Author
Parents
Loading