Commit 2026-04-14 17:36 c82b385c

View on Github →

feat(Analysis/SpecialFunctions/Complex/Circle): Circle.exp is InjOn intervals shorter than 2π (#37813) This Pr introduces injectivity and surjectivity of Circle.exp function:

  • exp_injOn_Icc
  • exp_injOn_Ico
  • exp_injOn_Ioc
  • exp_surjective

Estimated changes

added theorem Circle.exp_injOn_Icc
added theorem Circle.exp_injOn_Ico
added theorem Circle.exp_injOn_Ioc
added theorem Circle.exp_surjective