Commit 2025-03-26 20:16 02375584

View on Github →

feature(Analysis/SpecialFunctions/Trigonometric/Basic): basic facts about complex numbers (#23165) Adds some basic facts about complex numbers:

  • exp_pi_div_two_mul_I : Computes $e^{π/2i}$
  • exp_neg_pi_div_two_mul_I : Computes $e^{-π/2i}$
  • circleMap_pi_div_two : circleMap form of exp_pi_div_two_mul_I
  • circleMap_neg_pi_div_two : circleMap form of exp_neg_pi_div_two_mul_I
  • circleMap_zero_int_mul : circleMap form of exp_int_mul

Estimated changes

added theorem circleMap_zero_int_mul