Mathlib Changelog
v4
Changelog
About
Github
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