Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-25 17:43 5778df87

View on Github →

chore(analysis/complex/circle): upgrade exp_map_circle to continuous_map (#9942)

Estimated changes

modified def exp_map_circle
added theorem exp_map_circle_add
added theorem exp_map_circle_zero