Commit 2024-08-19 19:19 40f43217

View on Github →

feat(Circle): More basic lemmas (#15880) From LeanAPAP

Estimated changes

Modified Mathlib/Analysis/Complex/Circle.lean

added theorem Circle.coe_eq_one

added theorem Circle.coe_exp

added theorem Circle.coe_inj

added theorem Circle.coe_injective

deleted theorem Circle.exp_apply

added theorem Circle.ext

Modified Mathlib/Analysis/Fourier/AddCircle.lean

Modified Mathlib/Analysis/Normed/Algebra/Exponential.lean

added theorem Pi.coe_exp

deleted theorem Pi.exp_apply

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

added theorem Circle.exp_eq_one

added theorem Circle.exp_int_mul_two_pi

added theorem Circle.exp_two_pi_mul_int

Modified Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean