Theorem Complex.isTheta_exp_arg_mul_im

Modification history

2023-05-25 08:46

Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

feat: port Analysis.SpecialFunctions.Pow.Asymptotics (#4174)

Added Complex.isTheta_exp_arg_mul_im View on Github →