Commit 2023-05-21 12:23 7f9830ea

View on Github →

feat: port Analysis.SpecialFunctions.Complex.Circle (#4151)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

added theorem Real.Angle.arg_expMapCircle

added theorem Real.Angle.coe_expMapCircle

added theorem Real.Angle.expMapCircle_add

added theorem Real.Angle.expMapCircle_coe

added theorem Real.Angle.expMapCircle_neg

added theorem Real.Angle.expMapCircle_zero

added theorem arg_expMapCircle

added theorem circle.arg_eq_arg

added theorem circle.injective_arg

added theorem expMapCircle_add_two_pi

added theorem expMapCircle_arg

added theorem expMapCircle_eq_expMapCircle

added theorem expMapCircle_sub_two_pi

added theorem expMapCircle_two_pi

added theorem invOn_arg_expMapCircle

added theorem leftInverse_expMapCircle_arg

added theorem periodic_expMapCircle

added theorem surjOn_expMapCircle_neg_pi_pi