Commit 2025-03-25 01:16 8c33f6b5

View on Github →

refactor(Data/Complex/Exponential): Move circleMap into Data.Complex.Exponential (#23212) Move the definition of circleMap into Data/Complex/Exponential as suggested by #find_home. This would allow it to be used more widely earlier on.

Estimated changes

added theorem circleMap_mem_sphere'
added theorem circleMap_mem_sphere
added theorem circleMap_ne_center
added theorem circleMap_sub_center
added theorem circleMap_zero
added theorem circleMap_zero_radius
added theorem norm_circleMap_zero
added theorem periodic_circleMap
added def circleMap
deleted def circleMap
deleted theorem circleMap_eq_center_iff
deleted theorem circleMap_mem_closedBall
deleted theorem circleMap_mem_sphere'
deleted theorem circleMap_mem_sphere
deleted theorem circleMap_ne_center
deleted theorem circleMap_sub_center
deleted theorem circleMap_zero
deleted theorem circleMap_zero_radius
deleted theorem norm_circleMap_zero
deleted theorem periodic_circleMap