Commit 2025-04-02 17:04 3d845f2a

View on Github →

feat(Analysis/SpecialFunctions/Complex/CircleMap): some basic facts about circleMap (#23167) We move the definition of circleMap and some relative theorems to a new file. We also add some basic facts about it.

Estimated changes

added def circleMap
added theorem circleMap_mem_sphere'
added theorem circleMap_mem_sphere
added theorem circleMap_ne_center
added theorem circleMap_ne_mem_ball
added theorem circleMap_not_mem_ball
added theorem circleMap_pi_div_two
added theorem circleMap_sub_center
added theorem circleMap_zero
added theorem circleMap_zero_div
added theorem circleMap_zero_inv
added theorem circleMap_zero_mul
added theorem circleMap_zero_pow
added theorem circleMap_zero_radius
added theorem circleMap_zero_zpow
added theorem eq_of_circleMap_eq
added theorem norm_circleMap_zero
added theorem periodic_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_int_mul
deleted theorem circleMap_zero_radius
deleted theorem norm_circleMap_zero
deleted theorem periodic_circleMap
deleted def circleMap
deleted theorem circleMap_ne_mem_ball
deleted theorem circleMap_not_mem_ball